Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2

11 files changed, 80 insertions, 10 deletions

diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 9a09c57ec..8983e3e2b 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -570,6 +570,7 @@ REG0_TESTS = \
 	regress0/push-pop/boolean/fuzz_48.smt2 \
 	regress0/push-pop/boolean/fuzz_49.smt2 \
 	regress0/push-pop/boolean/fuzz_50.smt2 \
+	regress0/push-pop/bug1990.smt2 \
 	regress0/push-pop/bug233.cvc \
 	regress0/push-pop/bug654-dd.smt2 \
 	regress0/push-pop/bug691.smt2 \
@@ -805,6 +806,7 @@ REG0_TESTS = \
 	regress0/strings/str005.smt2 \
 	regress0/strings/strings-charat.cvc \
 	regress0/strings/strings-native-simple.cvc \
+	regress0/strings/strip-endpoint-itos.smt2 \
 	regress0/strings/substr-rewrites.smt2 \
 	regress0/strings/type001.smt2 \
 	regress0/strings/unsound-0908.smt2 \
@@ -1443,6 +1445,7 @@ REG1_TESTS = \
 	regress1/strings/idof-triv.smt2 \
 	regress1/strings/ilc-l-nt.smt2 \
 	regress1/strings/issue1105.smt2 \
+	regress1/strings/issue2060.smt2 \
 	regress1/strings/kaluza-fl.smt2 \
 	regress1/strings/loop002.smt2 \
 	regress1/strings/loop003.smt2 \
@@ -1562,7 +1565,8 @@ REG1_TESTS = \
 	regress1/uflia/microwave21.ec.minimized.smt2 \
 	regress1/uflia/simple_cyclic2.smt2 \
 	regress1/uflia/speed2_e8_449_e8_517.ec.smt2 \
-	regress1/uflia/stalmark_e7_27_e7_31.ec.smt2
+	regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 \
+	regress1/wrong-qfabvfp-smtcomp2018.smt2
 
 REG2_TESTS = \
 	regress2/DTP_k2_n35_c175_s15.smt2 \
diff --git a/test/regress/README.md b/test/regress/README.md
index d0c9b2b7a..772332c3e 100644
--- a/test/regress/README.md
+++ b/test/regress/README.md
@@ -116,10 +116,11 @@ a given benchmark when a feature is supported. For example:
 ; REQUIRES: symfpu
 ```
 
-This benchmark is only run when symfpu has been configured.
-Multiple `REQUIRES` directives are supported. For a list of
-features that can be listed as a requirement, refer to CVC4's
-`--show-config` output.
+This benchmark is only run when symfpu has been configured.  Multiple
+`REQUIRES` directives are supported. For a list of features that can be listed
+as a requirement, refer to CVC4's `--show-config` output. Features can also be
+excluded by adding the `no-` prefix, e.g. `no-symfpu` means that the test is
+not valid for builds that include symfpu support.
 
 Sometimes it is useful to keep the directives separate. You can separate the
 benchmark from the output expectations by putting the benchmark in `<benchmark
diff --git a/test/regress/regress0/push-pop/bug1990.smt2 b/test/regress/regress0/push-pop/bug1990.smt2
new file mode 100644
index 000000000..f0cde3113
--- /dev/null
+++ b/test/regress/regress0/push-pop/bug1990.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic QF_SAT)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(assert (or v1 v2))
+(check-sat)
+(assert false)
+(push)
+(check-sat)
+(pop)
+(check-sat)
diff --git a/test/regress/regress0/strings/strip-endpoint-itos.smt2 b/test/regress/regress0/strings/strip-endpoint-itos.smt2
new file mode 100644
index 000000000..c8d8c5af3
--- /dev/null
+++ b/test/regress/regress0/strings/strip-endpoint-itos.smt2
@@ -0,0 +1,7 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status sat)
+(declare-fun x () Int)
+(assert (str.contains "Ducati100" (int.to.str x)))
+(check-sat)
diff --git a/test/regress/regress1/arrayinuf_error.smt2 b/test/regress/regress1/arrayinuf_error.smt2
index 1fedd95ac..bc89dd0eb 100644
--- a/test/regress/regress1/arrayinuf_error.smt2
+++ b/test/regress/regress1/arrayinuf_error.smt2
@@ -1,4 +1,5 @@
-; EXPECT: (error "Parse Error: arrayinuf_error.smt2:7.21: Symbol 'Array' not declared as a type
+; REQUIRES: no-competition
+; EXPECT: (error "Parse Error: arrayinuf_error.smt2:8.21: Symbol 'Array' not declared as a type
 ; EXPECT: 
 ; EXPECT:   (declare-fun a (Array Bool Bool))
 ; EXPECT:                   ^
diff --git a/test/regress/regress1/datatypes/error.cvc b/test/regress/regress1/datatypes/error.cvc
index 23e658e6c..90c13c615 100644
--- a/test/regress/regress1/datatypes/error.cvc
+++ b/test/regress/regress1/datatypes/error.cvc
@@ -1,7 +1,7 @@
+% REQUIRES: no-competition
 % EXPECT-ERROR: CVC4 Error:
 % EXPECT-ERROR: Parse Error: foo already declared in this datatype
 % EXIT: 1
 
 DATATYPE single_ctor = foo(bar:REAL) | foo(bar2:REAL) END;
 DATATYPE double_ctor = foo(bar:REAL) END;
-
diff --git a/test/regress/regress1/error.cvc b/test/regress/regress1/error.cvc
index 8f76c798a..986527f98 100644
--- a/test/regress/regress1/error.cvc
+++ b/test/regress/regress1/error.cvc
@@ -1,6 +1,7 @@
+% REQUIRES: no-competition
 % ERROR-SCRUBBER: sed -e '/^[[:space:]]*$/d'
 % EXPECT-ERROR: CVC4 Error:
-% EXPECT-ERROR: Parse Error: error.cvc:6.8: Symbol 'BOOL' not declared as a type
+% EXPECT-ERROR: Parse Error: error.cvc:7.8: Symbol 'BOOL' not declared as a type
 % EXPECT-ERROR:   p : BOOL;
 % EXPECT-ERROR:       ^
 p : BOOL;
diff --git a/test/regress/regress1/errorcrash.smt2 b/test/regress/regress1/errorcrash.smt2
index 6b8a0a8f3..78df4324e 100644
--- a/test/regress/regress1/errorcrash.smt2
+++ b/test/regress/regress1/errorcrash.smt2
@@ -1,5 +1,6 @@
+; REQUIRES: no-competition
 ; EXIT: 1
-; EXPECT: (error "Parse Error: errorcrash.smt2:5.29: Symbol 'Array' not declared as a type")
+; EXPECT: (error "Parse Error: errorcrash.smt2:6.29: Symbol 'Array' not declared as a type")
 (set-logic QF_UF)
 (declare-sort U 0)
 (declare-fun x () (Array U U))
diff --git a/test/regress/regress1/strings/issue2060.smt2 b/test/regress/regress1/strings/issue2060.smt2
new file mode 100644
index 000000000..784fe1862
--- /dev/null
+++ b/test/regress/regress1/strings/issue2060.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-const action String)
+(declare-const example_key String)
+
+(assert (str.in.re action (re.++
+                           (str.to.re "foobar:ab")
+                           (re.* re.allchar)
+                   )))
+
+(declare-const action_1 String)
+(declare-const action_2 String)
+
+(assert (and
+         (= action (str.++ action_1 example_key action_2))
+         (= action_1 "foobar:a")
+         ))
+
+(check-sat)
diff --git a/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2 b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
new file mode 100644
index 000000000..3636b5795
--- /dev/null
+++ b/test/regress/regress1/wrong-qfabvfp-smtcomp2018.smt2
@@ -0,0 +1,15 @@
+; REQUIRES: symfpu
+; COMMAND-LINE: --decision=internal
+; COMMAND-LINE: --decision=justification
+; EXPECT: sat
+(set-info :smt-lib-version 2.6)
+(set-logic QF_BVFP)
+(declare-fun a () (_ BitVec 64))
+(declare-fun b () (_ BitVec 64))
+(assert (fp.leq ((_ to_fp 11 53) a) ((_ to_fp 11 53) (_ bv4626322717216342016 64))))
+(assert (not (fp.isNaN ((_ to_fp 11 53) b))))
+(declare-fun k2 () (_ BitVec 64))
+(assert (or (= k2 b) (= k2 a)))
+(assert
+(or (fp.isNaN ((_ to_fp 11 53) k2)) (fp.gt ((_ to_fp 11 53) k2) ((_ to_fp 11 53) (_ bv4626322717216342016 64))) ))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 9bd3de9f0..c29a97956 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -244,7 +244,13 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
         return
 
     for req_feature in requires:
-        if req_feature not in cvc4_features:
+        if req_feature.startswith("no-"):
+            inv_feature = req_feature[len("no-"):]
+            if inv_feature in cvc4_features:
+                print('1..0 # Skipped regression: not valid with {}'.format(
+                    inv_feature))
+                return
+        elif req_feature not in cvc4_features:
             print('1..0 # Skipped regression: {} not supported'.format(
                 req_feature))
             return