mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Fix minor problem

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-06-27 09:30:25 -07:00
parent f238720b76
commit 5b7201a911
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -23,7 +23,7 @@ Notes:
#include"smt_kernel.h" #include"smt_kernel.h"
#include"ast_pp.h" #include"ast_pp.h"
#include"mk_simplified_app.h" #include"mk_simplified_app.h"
#include"ast_util.h"
class ctx_solver_simplify_tactic : public tactic { class ctx_solver_simplify_tactic : public tactic {
ast_manager& m; ast_manager& m;
@ -104,7 +104,7 @@ protected:
return; return;
ptr_vector<expr> fmls; ptr_vector<expr> fmls;
g.get_formulas(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(); m_solver.push();
reduce(fml); reduce(fml);
m_solver.pop(1); m_solver.pop(1);
@ -119,7 +119,7 @@ protected:
{ {
m_solver.push(); m_solver.push();
expr_ref fml1(m); 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_iff(fml, fml1);
fml1 = m.mk_not(fml1); fml1 = m.mk_not(fml1);
m_solver.assert_expr(fml1); m_solver.assert_expr(fml1);