diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 11:53:07 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-05-11 11:53:07 +0200 |
commit | 870b29b0cce85941ed72d7e0ca75b61b0cfcf711 (patch) | |
tree | a4262ede90b2605b73c64ba4b52951d7cd708f72 /test/regress | |
parent | 2679806e54a0b265fae26eb9cf76a5f6a618e963 (diff) |
Add missing regression.
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) + |