From f1412d3f3249529224f4180f601652da210b274a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 28 Oct 2016 14:23:01 +0100 Subject: [PATCH] Bugfix for bouned_int2bv_solver --- src/tactic/portfolio/bounded_int2bv_solver.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index 8be0788e3..0b136dda7 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -294,6 +294,10 @@ private: for (unsigned i = 0; i < m_assertions.size(); ++i) { sub(m_assertions[i].get(), fml1); m_rewriter(fml1, fml2, proof); + if (m.canceled()) { + m_rewriter.reset(); + return; + } m_solver->assert_expr(fml2); TRACE("int2bv", tout << fml2 << "\n";); }