diff options
Diffstat (limited to 'test/regress/regress2/sygus/mpg_guard1-dd.sy')
| -rw-r--r-- | test/regress/regress2/sygus/mpg_guard1-dd.sy | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/test/regress/regress2/sygus/mpg_guard1-dd.sy b/test/regress/regress2/sygus/mpg_guard1-dd.sy index 31800a36f..98f13bb92 100644 --- a/test/regress/regress2/sygus/mpg_guard1-dd.sy +++ b/test/regress/regress2/sygus/mpg_guard1-dd.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic LIA) -(synth-fun eq1 ( (x Int) (y Int) ) Int +(synth-fun eq1 ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) ((Start Int (x y 0 @@ -13,15 +14,14 @@ (<= Start Start) (= Start Start))))) -(define-fun iteB (( b1 Bool ) (b2 Bool ) (b3 Bool )) Bool (or (and b1 b2) (and (not b1) b3))) +(define-fun iteB ((b1 Bool) (b2 Bool) (b3 Bool)) Bool (or (and b1 b2) (and (not b1) b3))) -(declare-var x Int) -(declare-var y Int) +(declare-var x Int) +(declare-var y Int) -(constraint (iteB (>= x 0) +(constraint (iteB (>= x 0) (= (eq1 x y) (+ x x)) - (= (eq1 x y) x) + (= (eq1 x y) x) )) (check-synth) - |