From 8c66691e6d411d9aa0e092843339d7f80983d39a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 3 Mar 2021 09:51:56 -0800 Subject: [PATCH] disable propagation in proof mode as it produces ill-formed proof objects. Fixes #5063 --- src/smt/asserted_formulas.cpp | 2 ++ src/tactic/core/propagate_values_tactic.cpp | 3 +++ 2 files changed, 5 insertions(+) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index bc5b47f7a..db387bf4c 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -525,6 +525,8 @@ void asserted_formulas::commit(unsigned new_qhead) { } void asserted_formulas::propagate_values() { + if (m.proofs_enabled()) + return; flush_cache(); unsigned num_prop = 0; diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp index 8ecee4ccf..6cf340e57 100644 --- a/src/tactic/core/propagate_values_tactic.cpp +++ b/src/tactic/core/propagate_values_tactic.cpp @@ -146,6 +146,9 @@ class propagate_values_tactic : public tactic { if (m_max_rounds == 0) goto end; + if (m_goal->proofs_enabled()) + goto end; + m_subst = alloc(expr_substitution, m, g->unsat_core_enabled(), g->proofs_enabled()); m_r.set_substitution(m_subst.get()); m_occs(*m_goal);