From bfe26390f01665c48f1cb2e9a297432bd0e06eba Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jun 2016 08:12:32 -0700 Subject: [PATCH] fix bug introduced when hiding unused variables in 96e157e, reported by Mikolas Janota Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_trailing.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bv_trailing.cpp b/src/ast/rewriter/bv_trailing.cpp index cf50ab0e2..31e9121ec 100644 --- a/src/ast/rewriter/bv_trailing.cpp +++ b/src/ast/rewriter/bv_trailing.cpp @@ -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;