diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-04-26 09:50:40 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2021-04-26 09:50:40 -0700 |
| commit | 94d015c59a80b1c0efe1eaca8f6fffec336eca55 (patch) | |
| tree | b3b4ccc3325727c061b37c7a39d670f57dd3ee55 | |
| parent | 0b1c90ac259085d9ee8911b422348254ea648771 (diff) | |
fix
| -rw-r--r-- | src/theory/rewriter/rules/basic.rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/rewriter/rules/basic.rules b/src/theory/rewriter/rules/basic.rules index 8c885849d..9fb964ebe 100644 --- a/src/theory/rewriter/rules/basic.rules +++ b/src/theory/rewriter/rules/basic.rules @@ -620,4 +620,4 @@ (define-rule UltPlusOne ( (n Int :const) (x (_ BitVec n)) (y (_ BitVec n))) (bvult x (bvadd y (_ bv 1 n))) - (and (not (bvult (bvnot y) x)) (not (= y (bvnot (_ bv 0 n)))))) + (and (not (bvult y x)) (not (= y (bvnot (_ bv 0 n)))))) |