diff options
Diffstat (limited to 'test/regress/regress2/sygus/mpg_guard1-dd.sy')
-rw-r--r-- | test/regress/regress2/sygus/mpg_guard1-dd.sy | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress2/sygus/mpg_guard1-dd.sy b/test/regress/regress2/sygus/mpg_guard1-dd.sy new file mode 100644 index 000000000..31800a36f --- /dev/null +++ b/test/regress/regress2/sygus/mpg_guard1-dd.sy @@ -0,0 +1,27 @@ +; EXPECT: unsat +; COMMAND-LINE: --sygus-out=status +(set-logic LIA) + +(synth-fun eq1 ( (x Int) (y Int) ) Int + ((Start Int (x + y + 0 + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (<= Start Start) + (= Start Start))))) + +(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) + +(constraint (iteB (>= x 0) + (= (eq1 x y) (+ x x)) + (= (eq1 x y) x) +)) + +(check-synth) + |