mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix non-termination

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-14 16:45:54 -07:00
parent 69a5634e7e
commit ff69ee049b
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/opt/optsmt.cpp
View file

@ -187,6 +187,17 @@ namespace opt {
tout << "\n"; tout << "\n";
model_pp(tout, *m_model); model_pp(tout, *m_model);
); );
IF_VERBOSE(2, verbose_stream() << "(optsmt.lower ";
for (unsigned i = 0; i < m_lower.size(); ++i) {
verbose_stream() << m_lower[i] << " ";
}
verbose_stream() << ")\n";);
for (unsigned i = 0; i < m_lower.size(); ++i) {
if (m_lower[i].is_pos() && !m_lower[i].is_finite()) {
disj[i] = m.mk_false();
}
}
expr_ref constraint(m); expr_ref constraint(m);
constraint = m.mk_or(disj.size(), disj.c_ptr()); constraint = m.mk_or(disj.size(), disj.c_ptr());
m_s->assert_expr(constraint); m_s->assert_expr(constraint);