summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc3.userdoc.02.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/cvc3.userdoc.02.cvc')
-rw-r--r--test/regress/regress0/cvc3.userdoc.02.cvc7
1 files changed, 0 insertions, 7 deletions
diff --git a/test/regress/regress0/cvc3.userdoc.02.cvc b/test/regress/regress0/cvc3.userdoc.02.cvc
deleted file mode 100644
index e143ea275..000000000
--- a/test/regress/regress0/cvc3.userdoc.02.cvc
+++ /dev/null
@@ -1,7 +0,0 @@
-x : BITVECTOR(5);
-y : BITVECTOR(4);
-yy : BITVECTOR(3);
-
-% EXPECT: entailed
-QUERY
- BVPLUS(9, x@0bin0000, (0bin000@(~y)@0bin11))[8:4] = BVPLUS(5, x, ~(y[3:2])) ;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback