diff options
Diffstat (limited to 'test/regress/regress0')
| -rwxr-xr-x | test/regress/regress0/sygus/General_plus10.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/array_search_2.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/c100.sy | 18 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/const-var-test.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/max.sy | 2 |
6 files changed, 24 insertions, 5 deletions
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index 33552f9e2..1792749e2 100755 --- a/test/regress/regress0/sygus/General_plus10.sy +++ b/test/regress/regress0/sygus/General_plus10.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun fb () Int ((Start Int ((Constant Int))))) diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 0d44a5214..9b9f1feb2 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -77,7 +77,8 @@ TESTS = commutative.sy \ strings-double-rec.sy \ hd-19-d1-prog-dup-op.sy \ real-grammar-neg.sy \ - real-si-all.sy + real-si-all.sy \ + c100.sy # disabled, takes too long with and without CBQI BV # Base16_1.sy diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 5786eb649..41346e655 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=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (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/c100.sy b/test/regress/regress0/sygus/c100.sy new file mode 100644 index 000000000..ef124c953 --- /dev/null +++ b/test/regress/regress0/sygus/c100.sy @@ -0,0 +1,18 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status + +(set-logic LIA) + +(synth-fun constant ((x Int)) Int + ((Start Int (0 + 2 + 3 + 5 + (+ Start Start) + (- Start Start) + )) + )) +(declare-var x Int) +(constraint (= (constant x) 100)) +(check-synth) + diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index af2d8b25b..305f5783a 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=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index cbe2bccea..37ed848ef 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=all --sygus-out=status --no-check-synth-sol +; COMMAND-LINE: --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int |