diff options
Diffstat (limited to 'test/regress/regress0/sets')
| -rw-r--r-- | test/regress/regress0/sets/sets-poly-nonint.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sets/sets-tuple-poly.cvc | 5 |
2 files changed, 3 insertions, 4 deletions
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; |