diff options
| author | lianah <lianahady@gmail.com> | 2013-03-23 17:19:21 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-23 17:19:21 -0400 |
| commit | b9b17625957d2e718dc2d071dff505d04ccad879 (patch) | |
| tree | 879e6250604321afb94d95992be8ffdca2240501 /test/regress/regress0/bv | |
| parent | 8882aef2dd4f1f629b0de99fc3a7f390fab2f83e (diff) | |
non-incremental inequality solver seems to be bug-free (i.e. passes fuzzing)
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/inequality04.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2 index 7b5dbd7d5..35607eaef 100644 --- a/test/regress/regress0/bv/inequality04.smt2 +++ b/test/regress/regress0/bv/inequality04.smt2 @@ -12,7 +12,7 @@ (bvule v0 v1) (bvule v1 v2) (bvule v2 v0) - (bvule (_ bv4 16) v0) + (bvult (_ bv4 16) v0) (bvult v2 (_ bv5 16)) )) (check-sat) |