blob: cade13fa361c8a588baf28ffe175a5f2cd6f0f31 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
(set-logic QF_AUFLIA)
(set-info :source |
Benchmarks used in the followin paper:
Big proof engines as little proof engines: new results on rewrite-based satisfiability procedure
Alessandro Armando, Maria Paola Bonacina, Silvio Ranise, Stephan Schulz.
PDPAR'05
http://www.ai.dist.unige.it/pdpar05/
|)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-fun a_705 () (Array Int Int))
(declare-fun a_707 () (Array Int Int))
(declare-fun a_709 () (Array Int Int))
(declare-fun a_711 () (Array Int Int))
(declare-fun a_713 () (Array Int Int))
(declare-fun a_715 () (Array Int Int))
(declare-fun a_717 () (Array Int Int))
(declare-fun a_719 () (Array Int Int))
(declare-fun a_721 () (Array Int Int))
(declare-fun a_723 () (Array Int Int))
(declare-fun a_725 () (Array Int Int))
(declare-fun a_727 () (Array Int Int))
(declare-fun a_728 () (Array Int Int))
(declare-fun a_729 () (Array Int Int))
(declare-fun e_704 () Int)
(declare-fun e_706 () Int)
(declare-fun e_708 () Int)
(declare-fun e_710 () Int)
(declare-fun e_712 () Int)
(declare-fun e_714 () Int)
(declare-fun e_716 () Int)
(declare-fun e_718 () Int)
(declare-fun e_720 () Int)
(declare-fun e_722 () Int)
(declare-fun e_724 () Int)
(declare-fun e_726 () Int)
(declare-fun e_731 () Int)
(declare-fun e_732 () Int)
(declare-fun i_730 () Int)
(declare-fun a1 () (Array Int Int))
(declare-fun i0 () Int)
(declare-fun i1 () Int)
(declare-fun i2 () Int)
(declare-fun i3 () Int)
(declare-fun i4 () Int)
(declare-fun i5 () Int)
(declare-fun sk ((Array Int Int) (Array Int Int)) Int)
(assert (= a_705 (store a1 i4 e_704)))
(assert (= a_707 (store a_705 i2 e_706)))
(assert (= a_709 (store a_707 i1 e_708)))
(assert (= a_711 (store a_709 i4 e_710)))
(assert (= a_713 (store a_711 i5 e_712)))
(assert (= a_715 (store a_713 i3 e_714)))
(assert (= a_717 (store a_715 i4 e_716)))
(assert (= a_719 (store a_717 i2 e_718)))
(assert (= a_721 (store a_719 i1 e_720)))
(assert (= a_723 (store a_721 i0 e_722)))
(assert (= a_725 (store a_723 i5 e_724)))
(assert (= a_727 (store a_725 i2 e_726)))
(assert (= a_728 (store a_723 i2 e_726)))
(assert (= a_729 (store a_728 i5 e_724)))
(assert (= e_704 (select a1 i2)))
(assert (= e_706 (select a1 i4)))
(assert (= e_708 (select a_707 i4)))
(assert (= e_710 (select a_707 i1)))
(assert (= e_712 (select a_711 i3)))
(assert (= e_714 (select a_711 i5)))
(assert (= e_716 (select a_715 i2)))
(assert (= e_718 (select a_715 i4)))
(assert (= e_720 (select a_719 i0)))
(assert (= e_722 (select a_719 i1)))
(assert (= e_724 (select a_723 i2)))
(assert (= e_726 (select a_723 i5)))
(assert (= e_731 (select a_727 i_730)))
(assert (= e_732 (select a_729 i_730)))
(assert (= i_730 (sk a_727 a_729)))
(assert (not (= e_731 e_732)))
(check-sat)
(exit)
|
