summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/qe.sy
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sygus/qe.sy')
-rw-r--r--test/regress/regress0/sygus/qe.sy12
1 files changed, 0 insertions, 12 deletions
diff --git a/test/regress/regress0/sygus/qe.sy b/test/regress/regress0/sygus/qe.sy
deleted file mode 100644
index 77e16efcb..000000000
--- a/test/regress/regress0/sygus/qe.sy
+++ /dev/null
@@ -1,12 +0,0 @@
-; 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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback