Add lazy strategy for bounded integers to avoid non-terminating unsat cases. Add regressions.

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)
+