Merge remote-tracking branch 'CVC4root/master'

7 files changed, 37 insertions, 11 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index ea74eb8ee..fe6b156f1 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -153,7 +153,8 @@ BUG_TESTS = \
 	bug522.smt2 \
 	bug528a.smt2 \
 	bug541.smt2 \
-	bug544.smt2
+	bug544.smt2 \
+	bug548a.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug548a.smt2 b/test/regress/regress0/bug548a.smt2
new file mode 100644
index 000000000..12658e507
--- /dev/null
+++ b/test/regress/regress0/bug548a.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --rewrite-divk --tlimit 1000
+; EXPECT: unknown
+(set-logic LIA)
+(declare-fun f (Int) Int)
+
+
+; instantiated version : cvc4 answers sat
+;(assert (= (f 1) (div 1 10)))
+;(assert (= (f 11) (div 11 10)))
+
+; cvc4 answers unsat, should be "sat", cvc4 expected to timeout or answer "unknown"
+(assert (forall ((x Int)) (= (f x) (div x 10))))
+
+(assert (= (f 1) 0))
+(assert (= (f 11) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index 2633949c8..b9a87231f 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -30,7 +30,8 @@ TESTS =	\
 	german73.smt2 \
 	PUZ001+1.smt2 \
 	refcount24.cvc.smt2 \
-	bug0909.smt2
+	bug0909.smt2 \
+	fmf-bound-int.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/fmf-bound-int.smt2 b/test/regress/regress0/fmf/fmf-bound-int.smt2
new file mode 100644
index 000000000..fb3106bdf
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-bound-int.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --finite-model-find --fmf-bound-int
+; EXPECT: sat
+(set-logic UFLIA)
+(declare-fun P (Int Int) Bool)
+(declare-fun Q (Int) Bool)
+(assert (forall ((x Int)) (=> (and (<= 0 x) (<= x (ite (P 0 0) 10 20))) (Q x))))
+(check-sat)
diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am
index 32f8a72ba..b7eac2535 100644
--- a/test/regress/regress0/rewriterules/Makefile.am
+++ b/test/regress/regress0/rewriterules/Makefile.am
@@ -25,7 +25,8 @@ TESTS =	\
 	length_trick.smt2 length_trick2.smt2 length_gen_020.smt2 \
 	datatypes.smt2 datatypes_sat.smt2 set_A_new_fast_tableau-base.smt2 \
 	set_A_new_fast_tableau-base_sat.smt2 relation.smt2 simulate_rewriting.smt2 \
-	reachability_back_to_the_future.smt2 native_arrays.smt2 reachability_bbttf_eT_arrays.smt2
+	reachability_back_to_the_future.smt2 native_arrays.smt2
+# reachability_bbttf_eT_arrays.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am
index 705a7eadb..e82076520 100644
--- a/test/regress/regress0/strings/Makefile.am
+++ b/test/regress/regress0/strings/Makefile.am
@@ -32,7 +32,6 @@ TESTS =	\
   fmf001.smt2 \
   fmf002.smt2 \
   type001.smt2 \
-  type002.smt2 \
   type003.smt2 \
   model001.smt2 \
   substr001.smt2 \
@@ -51,8 +50,8 @@ TESTS =	\
 
 FAILING_TESTS =
 
-EXTRA_DIST = $(TESTS)
-
+EXTRA_DIST = $(TESTS) \
+  type002.smt2
 
 # and make sure to distribute it
 EXTRA_DIST +=
diff --git a/test/regress/run_regression b/test/regress/run_regression
index ec9e17057..bf4dcc6ef 100755
--- a/test/regress/run_regression
+++ b/test/regress/run_regression
@@ -197,8 +197,8 @@ fi
 
 check_models=false
 if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then
-  if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models\>' &>/dev/null &&
-     ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models\>' &>/dev/null; then
+  if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null &&
+     ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then
     # later on, we'll run another test with --check-models on
     check_models=true
   fi
@@ -207,9 +207,9 @@ check_proofs=false
 if [ "$proof" = yes ]; then
   # proofs not currently supported in incremental mode, turn it off
   if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then
-    if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs\>' &>/dev/null &&
-       ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs\>' &>/dev/null &&
-       ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental\>' &>/dev/null &&
+    if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs' &>/dev/null &&
+       ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs' &>/dev/null &&
+       ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null &&
        ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then
       # later on, we'll run another test with --check-proofs on
       check_proofs=true