summaryrefslogtreecommitdiff
path: root/test/regress/regress0/ite_real_valid.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/ite_real_valid.smt')
-rw-r--r--test/regress/regress0/ite_real_valid.smt8
1 files changed, 0 insertions, 8 deletions
diff --git a/test/regress/regress0/ite_real_valid.smt b/test/regress/regress0/ite_real_valid.smt
deleted file mode 100644
index eeaaa17e0..000000000
--- a/test/regress/regress0/ite_real_valid.smt
+++ /dev/null
@@ -1,8 +0,0 @@
-(benchmark ite_real_valid
-:logic QF_LRA
-:status unsat
-:extrafuns ((x Real))
-:extrapreds ((b))
-:formula
- (not (implies (= x (ite b 0 1)) (>= x 0)))
-)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback