From 8d318e81b94daede5c9f226b60ff9e663d5ad181 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 27 Jun 2019 13:16:48 -0700 Subject: [PATCH] disable the assert that can fire because of the cube heuristic Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index b6024187e..8c700fe59 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1405,11 +1405,9 @@ std::ostream& core::print_terms(std::ostream& out) const { print_term(t, out) << std::endl; lpvar j = m_lar_solver.external_to_local(ext); SASSERT(j + 1); - SASSERT(value(t) == val(j)); - print_var(j, out); - out << "term again "; print_term(t, out) << std::endl; auto e = mk_expr(t); out << "e= " << e << "\n"; + print_var(j, out); } return out; }