diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/regress0/quantifiers/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/quantifiers/bi-artm-s.smt2 | 29 | ||||
-rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/strings/artemis-0512-nonterm.smt2 | 25 |
4 files changed, 58 insertions, 2 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index f12e67401..e399b4b23 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -41,7 +41,8 @@ TESTS = \ qcft-smtlib3dbc51.smt2 \ symmetric_unsat_7.smt2 \ javafe.ast.StmtVec.009.smt2 \ - ARI176e1.smt2 + ARI176e1.smt2 \ + bi-artm-s.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 diff --git a/test/regress/regress0/quantifiers/bi-artm-s.smt2 b/test/regress/regress0/quantifiers/bi-artm-s.smt2 new file mode 100644 index 000000000..5fb7522e9 --- /dev/null +++ b/test/regress/regress0/quantifiers/bi-artm-s.smt2 @@ -0,0 +1,29 @@ +; COMMAND-LINE: --fmf-bound-int-lazy +; EXPECT: unsat +(set-option :incremental "false") +(set-info :status unsat) +(set-logic ALL_SUPPORTED) +(declare-fun Y () String) +(set-info :notes "ufP_1 is uf type conv P") +(declare-fun ufP_1 (Int) Int) +(set-info :notes "ufM_2 is uf type conv M") +(declare-fun ufM_2 (Int) Int) +(declare-fun z1_3 () String) +(declare-fun z2_4 () String) +(declare-fun z3_5 () String) +(declare-fun V_253 () String) +(declare-fun V_254 () String) + +(assert (or (= Y "1") (= Y "0"))) +(assert (>= (ufP_1 0) 32)) +(assert + +(forall ((V_243 Int)) +(or +(not (and (>= V_243 0) (>= (+ (str.len Y) (* (- 1) V_243)) 1))) +(and +(or (not (= (str.len Y) (+ 1 V_243))) (= (ufP_1 V_243) (ufM_2 V_243))) +(not (>= (ufM_2 V_243) 10)) +(not (or (not (= (str.len Y) (+ 1 V_243 (str.len V_253)))) (not (= Y (str.++ V_253 (ite (= (ufM_2 V_243) 0) "0" "1") V_254)))) ))) )) + +(check-sat) diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index dd3c6b53a..ddc0eae7c 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -47,7 +47,8 @@ TESTS = \ loop007.smt2 \ loop008.smt2 \ loop009.smt2 \ - reloop.smt2 + reloop.smt2 \ + artemis-0512-nonterm.smt2 FAILING_TESTS = diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 new file mode 100644 index 000000000..ed97f36dd --- /dev/null +++ b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 @@ -0,0 +1,25 @@ +(set-logic QF_S) +(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) + |