mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

initialize solvers to ensure that eval mode has a solver

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-03-23 18:54:06 -07:00
parent 966a8f73d3
commit 753f2c89ef
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_parsers.cpp
View file

@ -21,8 +21,11 @@ Revision History:
#include "api/api_context.h" #include "api/api_context.h"
#include "api/api_util.h" #include "api/api_util.h"
#include "cmd_context/cmd_context.h" #include "cmd_context/cmd_context.h"
#include "smt/smt_solver.h"
#include "parsers/smt2/smt2parser.h" #include "parsers/smt2/smt2parser.h"
#include "solver/solver_na2as.h" #include "solver/solver_na2as.h"
#include "tactic/portfolio/smt_strategic_solver.h"
extern "C" { extern "C" {
@ -123,6 +126,7 @@ extern "C" {
LOG_Z3_eval_smtlib2_string(c, str); LOG_Z3_eval_smtlib2_string(c, str);
if (!mk_c(c)->cmd()) { if (!mk_c(c)->cmd()) {
mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m())); mk_c(c)->cmd() = alloc(cmd_context, false, &(mk_c(c)->m()));
mk_c(c)->cmd()->set_solver_factory(mk_smt_strategic_solver_factory());
} }
scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd(); scoped_ptr<cmd_context>& ctx = mk_c(c)->cmd();
std::string s(str); std::string s(str);