summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug167.smt
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/bug167.smt')
-rw-r--r--test/regress/regress0/bug167.smt19
1 files changed, 0 insertions, 19 deletions
diff --git a/test/regress/regress0/bug167.smt b/test/regress/regress0/bug167.smt
deleted file mode 100644
index 075cf3914..000000000
--- a/test/regress/regress0/bug167.smt
+++ /dev/null
@@ -1,19 +0,0 @@
-(benchmark tta_startup
-:logic QF_LRA
-:extrafuns ((x_62 Real))
-:extrafuns ((x_63 Real))
-:extrafuns ((x_65 Real))
-:extrafuns ((x_22 Real))
-:extrafuns ((x_21 Real))
-:extrafuns ((x_53 Real))
-:extrafuns ((x_54 Real))
-:status sat
-:formula
-(and
- (= x_54 (ite (= 2 x_53) x_22 x_21))
- (or (= 4 x_65) (= 3 x_65) (= 2 x_65) (= 1 x_65))
- (or (= 4 x_63) (= 1 x_63))
- (<= x_62 4)
- (or (= 1 x_62) (= 4 x_62))
-)
-)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback