mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
revert debug changes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9a642215eb
commit
eaffe46468
|
@ -1497,7 +1497,7 @@ lbool core::check(vector<lemma>& l_vec) {
|
|||
m_tangents.tangent_lemma();
|
||||
}
|
||||
|
||||
if (!done() && m_nla_settings.run_nra()) {
|
||||
if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {
|
||||
ret = m_nra.check();
|
||||
m_stats.m_nra_calls ++;
|
||||
}
|
||||
|
|
|
@ -73,8 +73,6 @@ struct solver::imp {
|
|||
}
|
||||
// TBD: add variable bounds?
|
||||
|
||||
m_nlsat->display(std::cout);
|
||||
|
||||
lbool r = l_undef;
|
||||
try {
|
||||
r = m_nlsat->check();
|
||||
|
|
Loading…
Reference in a new issue