summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/inequality00.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/bv/inequality00.smt2')
-rw-r--r--test/regress/regress0/bv/inequality00.smt24
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/bv/inequality00.smt2 b/test/regress/regress0/bv/inequality00.smt2
index 55e6786af..dc6285d52 100644
--- a/test/regress/regress0/bv/inequality00.smt2
+++ b/test/regress/regress0/bv/inequality00.smt2
@@ -9,11 +9,11 @@
(declare-fun v4 () (_ BitVec 16))
(declare-fun v5 () (_ BitVec 16))
(assert (and
+ (bvult v2 v4)
+ (bvult v3 v4)
(bvult v0 v1)
(bvult v1 v2)
(bvult v1 v3)
- (bvult v2 v4)
- (bvult v3 v4)
(bvult v4 v5)
(bvult v5 v1)
))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback