mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

fix bug introduced when hiding unused variables in 96e157e, reported by Mikolas Janota

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-06-14 08:12:32 -07:00
parent 8da0146318
commit bfe26390f0
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -67,10 +67,8 @@ struct bv_trailing::imp {
}
expr_ref out1(m);
expr_ref out2(m);
DEBUG_CODE(
const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
SASSERT(rm1 == min && rm2 == min););
VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH));
VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH));
const bool are_eq = m.are_equal(out1, out2);
result = are_eq ? m.mk_true() : m.mk_eq(out1, out2);
return are_eq ? BR_DONE : BR_REWRITE2;