diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-09 15:58:40 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-07-09 15:58:40 -0400 |
| commit | 211304a663417c69552ea9efc43aaef855d7cd70 (patch) | |
| tree | 31dd078fa74177f26bd7bc2f60227b9bbb6ac923 /test/regress/regress0/sets | |
| parent | b3c76399db741d8d616a75242345710dc1c1b81c (diff) | |
sets cvc parser
Diffstat (limited to 'test/regress/regress0/sets')
| -rw-r--r-- | test/regress/regress0/sets/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/sets/cvc-sample.cvc (renamed from test/regress/regress0/sets/cvc-sample.smt2) | 30 |
2 files changed, 18 insertions, 13 deletions
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 9536dfac1..19f6313fb 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -40,6 +40,7 @@ TESTS = \ mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \ mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \ copy_check_heap_access_33_4.smt2 \ + cvc-sample.cvc \ emptyset.smt2 \ error1.smt2 \ error2.smt2 \ diff --git a/test/regress/regress0/sets/cvc-sample.smt2 b/test/regress/regress0/sets/cvc-sample.cvc index 6f8b9f48b..c6fb95a77 100644 --- a/test/regress/regress0/sets/cvc-sample.smt2 +++ b/test/regress/regress0/sets/cvc-sample.cvc @@ -1,5 +1,17 @@ +% EXPECT: unsat +% EXPECT: unsat +% EXPECT: unsat +% EXPECT: unsat +% EXPECT: unsat +% EXPECT: valid +OPTION "incremental" true; OPTION "logic" "ALL_SUPPORTED"; SetInt : TYPE = SET OF INT; +x : SET OF INT; +y : SET OF INT; +z : SET OF INT; +e1 : INT; +e2 : INT; PUSH; a : SET OF INT; b : SET OF INT; @@ -16,18 +28,11 @@ ASSERT e IN (a & b); CHECKSAT TRUE; POP; PUSH; -x : SET OF INT; -y : SET OF INT; -z : SET OF INT; ASSERT x = y; ASSERT NOT((x | z) = (y | z)); CHECKSAT TRUE; POP; PUSH; -x : SET OF INT; -y : SET OF INT; -e1 : INT; -e2 : INT; ASSERT x = y; ASSERT e1 = e2; ASSERT e1 IN x; @@ -35,11 +40,6 @@ ASSERT NOT(e2 IN y); CHECKSAT TRUE; POP; PUSH; -x : SET OF INT; -y : SET OF INT; -z : SET OF INT; -e1 : INT; -e2 : INT; ASSERT x = y; ASSERT e1 = e2; ASSERT e1 IN (x | z); @@ -50,4 +50,8 @@ PUSH; ASSERT 5 IN ({1, 2, 3, 4} | {5}); ASSERT 5 IN ({1, 2, 3, 4} | {} :: SET OF INT); CHECKSAT TRUE; - +POP; +PUSH; +QUERY LET v_0 = e1 IN z +IN NOT (v_0 AND NOT v_0); +POP; |