From 155738088fb8b55840e4ed9227f4295edbbb4a1a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Mar 2021 17:20:39 -0700 Subject: [PATCH] fix internalization on post-visit, increase delay to 100 --- src/sat/smt/euf_internalize.cpp | 1 + src/sat/smt/sat_th.cpp | 2 +- src/smt/params/smt_params_helper.pyg | 2 +- 3 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp index c2e5c26ec..e98129710 100644 --- a/src/sat/smt/euf_internalize.cpp +++ b/src/sat/smt/euf_internalize.cpp @@ -92,6 +92,7 @@ namespace euf { m_args.push_back(m_egraph.find(to_app(e)->get_arg(i))); if (root && internalize_root(to_app(e), sign, m_args)) return false; + SASSERT(!get_enode(e)); if (auto* s = expr2solver(e)) s->internalize(e, m_is_redundant); else diff --git a/src/sat/smt/sat_th.cpp b/src/sat/smt/sat_th.cpp index da668643d..bebe9ad5d 100644 --- a/src/sat/smt/sat_th.cpp +++ b/src/sat/smt/sat_th.cpp @@ -45,7 +45,7 @@ namespace euf { if (!visit(arg)) goto loop; } - if (!post_visit(e, sign, root && a == e)) + if (!visited(e) && !post_visit(e, sign, root && a == e)) return false; m_stack.pop_back(); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 55d4f9f9e..c789bf0cc 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -71,7 +71,7 @@ def_module_params(module_name='smt', ('arith.nl.grobner_cnfl_to_report', UINT, 1, 'grobner\'s maximum number of conflicts to report'), ('arith.nl.gr_q', UINT, 10, 'grobner\'s quota'), ('arith.nl.grobner_subs_fixed', UINT, 2, '0 - no subs, 1 - substitute, 2 - substitute fixed zeros only'), - ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'), + ('arith.nl.delay', UINT, 100, 'number of calls to final check before invoking bounded nlsat check'), ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'), ('arith.propagation_mode', UINT, 1, '0 - no propagation, 1 - propagate existing literals, 2 - refine finite bounds'), ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),