diff options
Diffstat (limited to 'test/regress/regress1/rels/bv1-unitb.cvc.smt2')
| -rw-r--r-- | test/regress/regress1/rels/bv1-unitb.cvc.smt2 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test/regress/regress1/rels/bv1-unitb.cvc.smt2 b/test/regress/regress1/rels/bv1-unitb.cvc.smt2 index c1db4195f..696c8919e 100644 --- a/test/regress/regress1/rels/bv1-unitb.cvc.smt2 +++ b/test/regress/regress1/rels/bv1-unitb.cvc.smt2 @@ -12,8 +12,8 @@ (declare-fun e () (_ BitVec 1)) (declare-fun u () unitb) (assert (not (= b c))) -(assert (member (mkTuple a u b) x)) -(assert (member (mkTuple a u c) x)) -(assert (member (mkTuple d u a) y)) -(assert (not (member (mkTuple a u u a) (join x y)))) +(assert (member (tuple a u b) x)) +(assert (member (tuple a u c) x)) +(assert (member (tuple d u a) y)) +(assert (not (member (tuple a u u a) (join x y)))) (check-sat) |