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/regress/regress0/sets | |
| 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/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; |