From 8b8caf9dedc41f38a8c16d024cecfe27beee6909 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Aug 2022 18:19:30 -0700 Subject: [PATCH] re-add smt-solver for proof_cmds Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/proof_cmds.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/extra_cmds/proof_cmds.cpp b/src/cmd_context/extra_cmds/proof_cmds.cpp index 8b61f1914..cd263554a 100644 --- a/src/cmd_context/extra_cmds/proof_cmds.cpp +++ b/src/cmd_context/extra_cmds/proof_cmds.cpp @@ -24,7 +24,7 @@ Notes: #include "util/small_object_allocator.h" #include "ast/ast_util.h" #include "cmd_context/cmd_context.h" -// include "smt/smt_solver.h" +#include "smt/smt_solver.h" // include "sat/sat_solver.h" // include "sat/sat_drat.h" #include "sat/smt/euf_proof_checker.h" @@ -57,7 +57,7 @@ public: // sat_solver(m_params, m.limit()), // m_drat(sat_solver) { -// m_solver = mk_smt_solver(m, m_params, symbol()); + m_solver = mk_smt_solver(m, m_params, symbol()); } void check(expr_ref_vector const& clause, expr* proof_hint) {