mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Bugfix for bouned_int2bv_solver

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2016-10-28 14:23:01 +01:00
parent 02e1bae9cb
commit f1412d3f32
1 changed files with 4 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -294,6 +294,10 @@ private:
for (unsigned i = 0; i < m_assertions.size(); ++i) { for (unsigned i = 0; i < m_assertions.size(); ++i) {
sub(m_assertions[i].get(), fml1); sub(m_assertions[i].get(), fml1);
m_rewriter(fml1, fml2, proof); m_rewriter(fml1, fml2, proof);
if (m.canceled()) {
m_rewriter.reset();
return;
}
m_solver->assert_expr(fml2); m_solver->assert_expr(fml2);
TRACE("int2bv", tout << fml2 << "\n";); TRACE("int2bv", tout << fml2 << "\n";);
} }