diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-02-02 15:34:44 -0600 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-02 15:34:44 -0600 |
| commit | 73a92766063e76e6c6f2507f126fb8f84ed3e432 (patch) | |
| tree | 22b3fc7b54ab32af44f5670d4c1852a9ec4c537f /test/regress/regress0/sygus | |
| parent | 64192c63a0011e4737eec2d27cf4deabf74d6c0a (diff) | |
Option to check solutions produced by SyGuS solver (#1553)
Diffstat (limited to 'test/regress/regress0/sygus')
| -rwxr-xr-x | test/regress/regress0/sygus/General_plus10.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/array_search_2.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/const-var-test.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/max.sy | 2 |
4 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy index 1792749e2..33552f9e2 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 +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) (synth-fun fb () Int ((Start Int ((Constant Int))))) diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy index 41346e655..5786eb649 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 +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (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/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy index 305f5783a..af2d8b25b 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 +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy index 37ed848ef..cbe2bccea 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 +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int |