summaryrefslogtreecommitdiff
path: root/test/regress/regress0/cvc3.userdoc.05.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/cvc3.userdoc.05.cvc')
-rw-r--r--test/regress/regress0/cvc3.userdoc.05.cvc2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/cvc3.userdoc.05.cvc b/test/regress/regress0/cvc3.userdoc.05.cvc
index 37da96b3c..85e0c2105 100644
--- a/test/regress/regress0/cvc3.userdoc.05.cvc
+++ b/test/regress/regress0/cvc3.userdoc.05.cvc
@@ -3,7 +3,7 @@ x, y : BITVECTOR(4);
ASSERT x = 0hex5;
ASSERT y = 0bin0101;
-% EXPECT: valid
+% EXPECT: entailed
QUERY
BVMULT(8,x,y)=BVMULT(8,y,x)
AND
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback