diff options
Diffstat (limited to 'test/regress/regress0/sets/mar2014/sharing-preregister.smt2')
| -rw-r--r-- | test/regress/regress0/sets/mar2014/sharing-preregister.smt2 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 index dc42abfa2..d851ca35e 100644 --- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 +++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 @@ -1,12 +1,12 @@ ; EXPECT: unsat -(set-logic QF_UFLIA_SETS) +(set-logic QF_UFLIAFS) (set-info :status sat) (declare-fun a () Int) (declare-fun b () Int) (declare-fun x () (Set Int)) (declare-fun y () (Set Int)) -(assert (= x (setenum a))) -(assert (= y (setenum b))) +(assert (= x (singleton a))) +(assert (= y (singleton b))) (assert (not (= x y))) (assert (and (< 1 a) (< a 3) (< 1 b) (< b 3))) (check-sat) |