diff options
Diffstat (limited to 'test')
26 files changed, 73 insertions, 73 deletions
diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 5d8cd8752..56a30b210 100644 --- a/test/regress/regress0/sygus/array_search_2.sy +++ b/test/regress/regress0/sygus/array_search_2.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy index 48b5c8a4d..f6c0320e2 100644 --- a/test/regress/regress0/sygus/array_sum_2_5.sy +++ b/test/regress/regress0/sygus/array_sum_2_5.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start))))) (declare-var x1 Int) diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy index 15567b0a8..46dbd2981 100644 --- a/test/regress/regress0/sygus/commutative.sy +++ b/test/regress/regress0/sygus/commutative.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 0d753bdf1..428cb2adc 100644 --- a/test/regress/regress0/sygus/const-var-test.sy +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy index ddc12a6a9..0059f6947 100644 --- a/test/regress/regress0/sygus/constant.sy +++ b/test/regress/regress0/sygus/constant.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy index dbf415986..e5448d626 100644 --- a/test/regress/regress0/sygus/dup-op.sy +++ b/test/regress/regress0/sygus/dup-op.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ Start Start) x)) diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy index 52a72c07d..cd129385e 100644 --- a/test/regress/regress0/sygus/enum-test.sy +++ b/test/regress/regress0/sygus/enum-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (define-sort D (Enum (a b))) (define-fun f ((x D)) Int (ite (= x D::a) 3 7)) diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy index a58bc2f64..2e6c6ef81 100644 --- a/test/regress/regress0/sygus/hd-01-d1-prog.sy +++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic BV) @@ -8,12 +8,12 @@ (synth-fun f ((x (BitVec 32))) (BitVec 32) ((Start (BitVec 32) ((bvand Start Start) (bvsub Start Start) - (bvor Start Start) - (bvadd Start Start) - (bvxor Start Start) + (bvor Start Start) + (bvadd Start Start) + (bvxor Start Start) x - #x00000000 - #xFFFFFFFF + #x00000000 + #xFFFFFFFF #x00000001)))) (declare-var x (BitVec 32)) diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy index 6e1610337..b07be0e98 100644 --- a/test/regress/regress0/sygus/icfp_28_10.sy +++ b/test/regress/regress0/sygus/icfp_28_10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic BV) @@ -14,14 +14,14 @@ (Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start) (shl1 Start) - (shr1 Start) - (shr4 Start) - (shr16 Start) - (bvand Start Start) - (bvor Start Start) - (bvxor Start Start) - (bvadd Start Start) - (if0 Start Start Start) + (shr1 Start) + (shr4 Start) + (shr16 Start) + (bvand Start Start) + (bvor Start Start) + (bvxor Start Start) + (bvadd Start Start) + (if0 Start Start Start) )) ) ) diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy index dda8e0ed5..aafbbd987 100644 --- a/test/regress/regress0/sygus/inv-example.sy +++ b/test/regress/regress0/sygus/inv-example.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-inv inv-f ((x Int) (y Int) (b Bool))) (declare-primed-var x Int) diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy index 046d074d9..4bae90b00 100644 --- a/test/regress/regress0/sygus/let-ringer.sy +++ b/test/regress/regress0/sygus/let-ringer.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (define-fun g ((x Int)) Int (ite (= x 1) 15 19)) (synth-fun f ((x Int)) Int diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy index daca906a2..71cd27e8f 100644 --- a/test/regress/regress0/sygus/let-simp.sy +++ b/test/regress/regress0/sygus/let-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int) (y Int)) Int ((Start Int (x diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index 4fc515353..dec4594d7 100644 --- a/test/regress/regress0/sygus/max.sy +++ b/test/regress/regress0/sygus/max.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy index 24d49ee4e..6d185ba3f 100644 --- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy +++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy @@ -1,13 +1,13 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun addExpr1 ((x Int) (y Int)) Int ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) @@ -16,8 +16,8 @@ (synth-fun addExpr2 ((x Int) (y Int)) Int ((Start Int (x y - 0 - 1 + 0 + 1 (+ Start Start) (- Start Start) )) diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy index bd7c79e3e..9065a1025 100644 --- a/test/regress/regress0/sygus/nflat-fwd-3.sy +++ b/test/regress/regress0/sygus/nflat-fwd-3.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ (+ Con Con) Con) x)) diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy index 0f9d46215..d211d475b 100644 --- a/test/regress/regress0/sygus/nflat-fwd.sy +++ b/test/regress/regress0/sygus/nflat-fwd.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x)) diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy index 81f90e2aa..cb284b180 100755 --- a/test/regress/regress0/sygus/no-flat-simp.sy +++ b/test/regress/regress0/sygus/no-flat-simp.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy index cc3855ad1..4b3fa22e6 100644 --- a/test/regress/regress0/sygus/no-syntax-test-bool.sy +++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy index 21788426c..86b60638b 100644 --- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy +++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy index 95f9b7c11..b95f31aa7 100644 --- a/test/regress/regress0/sygus/no-syntax-test.sy +++ b/test/regress/regress0/sygus/no-syntax-test.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy index c4fbd1c17..03d180634 100644 --- a/test/regress/regress0/sygus/parity-AIG-d0.sy +++ b/test/regress/regress0/sygus/parity-AIG-d0.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic BV) (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy index a8da13742..1545f86cd 100644 --- a/test/regress/regress0/sygus/tl-type.sy +++ b/test/regress/regress0/sygus/tl-type.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi --no-cegqi-si +; COMMAND-LINE: --cegqi --no-cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int (Term (+ Start Start))) diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy index 24b0f2c09..7f84ce06c 100644 --- a/test/regress/regress0/sygus/twolets1.sy +++ b/test/regress/regress0/sygus/twolets1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) ;; f1 is x plus 2 ;; f2 is 2x plus 5 @@ -7,27 +7,27 @@ (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z)) (synth-fun f1 ((x Int)) Int - ( - (Start Int ( - (let0 Intx CInt CInt) - ) - ) - (Intx Int (x)) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - - ) + ( + (Start Int ( + (let0 Intx CInt CInt) + ) + ) + (Intx Int (x)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + + ) ) (synth-fun f2 ((x Int)) Int - ( - (Start Int (x - (let0 Intx Start CInt) - ) - ) + ( + (Start Int (x + (let0 Intx Start CInt) + ) + ) (Intx Int (x)) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy index c1066277e..91bab5ece 100644 --- a/test/regress/regress0/sygus/twolets2-orig.sy +++ b/test/regress/regress0/sygus/twolets2-orig.sy @@ -1,25 +1,25 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si +; COMMAND-LINE: --cegqi-si --no-dump-synth (set-logic LIA) (synth-fun f1 ((x Int)) Int - ( - (Start Int ( - (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) - ) - ) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + ( + (Start Int ( + (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) (synth-fun f2 ((x Int)) Int - ( - (Start Int (x - (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) - ) - ) - (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) + ( + (Start Int (x + (let ((y Int Start) (z Int CInt)) (+ (+ y x) z)) + ) + ) + (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15)) - ) + ) ) (declare-var x1 Int) (declare-var x2 Int) diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy index b020c0bee..9886f6a7b 100644 --- a/test/regress/regress0/sygus/uminus_one.sy +++ b/test/regress/regress0/sygus/uminus_one.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun f ((x Int)) Int ((Start Int ((- 1))))) (declare-var x Int) diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy index dc39efd84..7c9d6c601 100644 --- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy +++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi +; COMMAND-LINE: --cegqi --no-dump-synth (set-logic LIA) (synth-fun inv ((x Int)) Bool |