summaryrefslogtreecommitdiff
path: root/test/regress/regress0/ineq_basic.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/ineq_basic.smt')
-rw-r--r--test/regress/regress0/ineq_basic.smt9
1 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/regress0/ineq_basic.smt b/test/regress/regress0/ineq_basic.smt
new file mode 100644
index 000000000..ba4cb8b7f
--- /dev/null
+++ b/test/regress/regress0/ineq_basic.smt
@@ -0,0 +1,9 @@
+(benchmark ineq_basic
+:status unsat
+:logic QF_LRA
+:extrafuns ((x Real))
+:formula
+ (and (<= 0 x)
+ (< x 0)
+ )
+)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback