mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

More work on trailing 0 analysis.

Browse source
This commit is contained in:
mikolas 2016-04-03 18:27:56 +01:00 • committed by Mikolas Janota
parent 78cb1e3c7b
commit ddb6ae4eab
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bv_trailing.cpp
View file

@ -46,7 +46,7 @@ struct bv_trailing::imp {
unsigned max1, min1, max2, min2;
count_trailing(e1, min1, max1, TRAILING_DEPTH);
count_trailing(e2, min2, max2, TRAILING_DEPTH);
if (min1 > max2 || min2 > max2) {
if (min1 > max2 || min2 > max1) {
result = m().mk_false();
return BR_DONE;
}