diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/sygus/const-var-test.sy | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy new file mode 100644 index 000000000..0d753bdf1 --- /dev/null +++ b/test/regress/regress0/sygus/const-var-test.sy @@ -0,0 +1,26 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si + +(set-logic LIA) + +(synth-fun max2 ((x Int) (y Int)) Int + ((Start Int ((Variable Int) + (Constant Int) + (+ Start Start) + (- Start Start) + (ite StartBool Start Start))) + (StartBool Bool ((and StartBool StartBool) + (or StartBool StartBool) + (not StartBool) + (<= Start Start) + (= Start Start) + (>= Start Start))))) + +(declare-var x Int) +(declare-var y Int) + +(constraint (= (max2 x y) (+ x y 500))) + + +(check-synth) + |