diff options
Diffstat (limited to 'test/regress')
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; |