diff options
Diffstat (limited to 'test/regress/regress1/sygus/qe.sy')
| -rw-r--r-- | test/regress/regress1/sygus/qe.sy | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/sygus/qe.sy b/test/regress/regress1/sygus/qe.sy new file mode 100644 index 000000000..77e16efcb --- /dev/null +++ b/test/regress/regress1/sygus/qe.sy @@ -0,0 +1,12 @@ +; EXPECT: unsat +; COMMAND-LINE: --cegqi-si=all --sygus-out=status --sygus-qe-preproc +(set-logic LIA) + +(synth-fun f ((x Int)) Int) + +(declare-var x Int) +(declare-var y Int) + +(constraint (=> (or (= y 2) (= y 3)) (> (f x) y))) + +(check-synth) |