From 5b7201a911a0e5f0e4efabc143ebac4be6e41c13 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 27 Jun 2013 09:30:25 -0700 Subject: [PATCH] Fix minor problem Signed-off-by: Leonardo de Moura --- src/smt/tactic/ctx_solver_simplify_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp index 5668ca455..63c14f297 100644 --- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp +++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp @@ -23,7 +23,7 @@ Notes: #include"smt_kernel.h" #include"ast_pp.h" #include"mk_simplified_app.h" - +#include"ast_util.h" class ctx_solver_simplify_tactic : public tactic { ast_manager& m; @@ -104,7 +104,7 @@ protected: return; ptr_vector fmls; g.get_formulas(fmls); - fml = m.mk_and(fmls.size(), fmls.c_ptr()); + fml = mk_and(m, fmls.size(), fmls.c_ptr()); m_solver.push(); reduce(fml); m_solver.pop(1); @@ -119,7 +119,7 @@ protected: { m_solver.push(); expr_ref fml1(m); - fml1 = m.mk_and(fmls.size(), fmls.c_ptr()); + fml1 = mk_and(m, fmls.size(), fmls.c_ptr()); fml1 = m.mk_iff(fml, fml1); fml1 = m.mk_not(fml1); m_solver.assert_expr(fml1);