From ff69ee049b5f210633bd3938a34d6e8704028966 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Oct 2014 16:45:54 -0700 Subject: [PATCH] fix non-termination Signed-off-by: Nikolaj Bjorner --- src/opt/optsmt.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 0d82e4410..37c7673df 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -187,6 +187,17 @@ namespace opt { tout << "\n"; 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); constraint = m.mk_or(disj.size(), disj.c_ptr()); m_s->assert_expr(constraint);