From 5c2a381eb03085785805a721bfaa43b8d66e1634 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Apr 2020 11:46:37 -0700 Subject: [PATCH] fix #3654 Signed-off-by: Nikolaj Bjorner --- src/smt/tactic/unit_subsumption_tactic.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/tactic/unit_subsumption_tactic.cpp b/src/smt/tactic/unit_subsumption_tactic.cpp index 9be3dd83a..812b79740 100644 --- a/src/smt/tactic/unit_subsumption_tactic.cpp +++ b/src/smt/tactic/unit_subsumption_tactic.cpp @@ -40,7 +40,8 @@ struct unit_subsumption_tactic : public tactic { void cleanup() override {} void operator()(/* in */ goal_ref const & in, - /* out */ goal_ref_buffer & result) override { + /* out */ goal_ref_buffer & result) override { + fail_if_proof_generation("unit-subsumption", in); reduce_core(in, result); } @@ -106,7 +107,7 @@ struct unit_subsumption_tactic : public tactic { } void insert_result(goal_ref& result) { - for (auto d : m_deleted) result->update(d, m.mk_true()); // TBD proof? + for (auto d : m_deleted) result->update(d, m.mk_true()); } void init(goal_ref const& g) {