diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:02:51 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-30 09:03:20 -0500 |
| commit | 303b91f3f5b8df1a884566a7d433ced17f0cd352 (patch) | |
| tree | ebe6334ca8a415a4d5a24a83ee40441419c93876 /test | |
| parent | ae1d4e4f05fdc2db61d7de7efee5bd567363ceef (diff) | |
Minor change to trigger selection, fixes related to subtypes (in macros, cbqi, tptp parser), fix full saturation instantiation to not loop in rare case, update regressions, update casc scripts.
Diffstat (limited to 'test')
6 files changed, 9 insertions, 12 deletions
diff --git a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 index 20de79047..586aa64c7 100644 --- a/test/regress/regress0/quantifiers/macro-subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/macro-subtype-param.smt2 @@ -1,18 +1,17 @@ ; COMMAND-LINE: --macros-quant ; EXPECT: unknown -; this will fail if type rule for APPLY_UF requires to be subtypes (set-logic ALL_SUPPORTED) (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) -(declare-fun R ((List Int)) Bool) +(declare-fun R ((List Real)) Bool) (assert (forall ((x (List Int))) (R x))) (declare-fun j1 () (List Real)) (assert (not (R j1))) -(declare-fun Q ((Array Real Int)) Bool) +(declare-fun Q ((Array Int Real)) Bool) (assert (forall ((x (Array Real Int))) (Q x))) -(declare-fun j2 () (Array Int Real)) +(declare-fun j2 () (Array Real Real)) (assert (not (Q j2))) (check-sat) diff --git a/test/regress/regress0/quantifiers/macros-real-arg.smt2 b/test/regress/regress0/quantifiers/macros-real-arg.smt2 index 675c96d68..edacdbe37 100644 --- a/test/regress/regress0/quantifiers/macros-real-arg.smt2 +++ b/test/regress/regress0/quantifiers/macros-real-arg.smt2 @@ -6,6 +6,6 @@ (assert (forall ((x Int)) (P x))) (declare-fun k () Real) (declare-fun k2 () Int) -(assert (or (not (P k)) (not (P k2)))) +(assert (or (not (P (to_int k))) (not (P k2)))) (assert (= k 0)) (check-sat) diff --git a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 index 836449cb9..42cfb3a11 100644 --- a/test/regress/regress0/quantifiers/subtype-param-unk.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param-unk.smt2 @@ -5,8 +5,7 @@ (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) -(declare-fun R ((List Int)) Bool) - +(declare-fun R ((List Real)) Bool) (assert (forall ((x (List Int))) (R x))) (declare-fun j1 () (List Real)) (assert (not (R j1))) diff --git a/test/regress/regress0/quantifiers/subtype-param.smt2 b/test/regress/regress0/quantifiers/subtype-param.smt2 index 08615abf6..a7fe58ac9 100644 --- a/test/regress/regress0/quantifiers/subtype-param.smt2 +++ b/test/regress/regress0/quantifiers/subtype-param.smt2 @@ -3,7 +3,7 @@ (declare-datatypes (T) ((List (cons (hd T) (tl (List T))) (nil)))) -(declare-fun R ((List Int)) Bool) +(declare-fun R ((List Real)) Bool) (assert (forall ((x (List Real))) (R x))) (declare-fun Q ((Array Int Real)) Bool) diff --git a/test/regress/regress0/sets/sets-poly-nonint.smt2 b/test/regress/regress0/sets/sets-poly-nonint.smt2 index 441716dcf..a0e883ace 100644 --- a/test/regress/regress0/sets/sets-poly-nonint.smt2 +++ b/test/regress/regress0/sets/sets-poly-nonint.smt2 @@ -7,5 +7,5 @@ (assert (member 1.5 t)) (assert (member 2.5 r)) (assert (member 3.5 u)) -(assert (or (member 4.5 s) (= s t) (= s r) (= s u) (= s (singleton 6.5)))) +(assert (or (= s t) (= s r) (= s u))) (check-sat) diff --git a/test/regress/regress0/sets/sets-tuple-poly.cvc b/test/regress/regress0/sets/sets-tuple-poly.cvc index 8d87345f6..64fb310be 100644 --- a/test/regress/regress0/sets/sets-tuple-poly.cvc +++ b/test/regress/regress0/sets/sets-tuple-poly.cvc @@ -7,11 +7,10 @@ b : SET OF [INT, REAL]; x : [ REAL, REAL ]; - ASSERT NOT x = (0,0); -ASSERT x IS_IN a; -ASSERT x IS_IN b; +ASSERT (x.0, FLOOR(x.1)) IS_IN a; +ASSERT (FLOOR(x.0), x.1) IS_IN b; ASSERT NOT x.0 = x.1; |