summaryrefslogtreecommitdiff
path: root/test/regress/regress0/strings/artemis-0512-nonterm.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/strings/artemis-0512-nonterm.smt2')
-rw-r--r--test/regress/regress0/strings/artemis-0512-nonterm.smt226
1 files changed, 0 insertions, 26 deletions
diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2
deleted file mode 100644
index 4b1cad8f6..000000000
--- a/test/regress/regress0/strings/artemis-0512-nonterm.smt2
+++ /dev/null
@@ -1,26 +0,0 @@
-(set-logic QF_S)
-(set-option :strings-exp true)
-(set-info :status unsat)
-
-(declare-const Y String)
-(assert
- (or
- (= Y "01")
- (= Y "02")
- (= Y "03")
- (= Y "04")
- (= Y "05")
- (= Y "06")
- (= Y "07")
- (= Y "08")
- (= Y "09")
- (= Y "10")
- (= Y "11")
- (= Y "12")
- )
-)
-
-(assert (= (<= (str.to.int Y) 31) false))
-
-(check-sat)
-
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback