Skip to content

Commit

Permalink
Fix printing solver creation for MathSAT (#368)
Browse files Browse the repository at this point in the history
  • Loading branch information
CyanoKobalamyne authored Jan 31, 2025
1 parent 97ab021 commit d6a81c5
Showing 1 changed file with 10 additions and 8 deletions.
18 changes: 10 additions & 8 deletions smt/available_solvers.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -136,12 +136,8 @@ SmtSolver create_solver_for(
full_model = true;
}

if (se != MSAT) {
// no special options yet for solvers other than mathsat
s = create_solver(se, logging, true, true, printing);
}
#ifdef WITH_MSAT
else if (se == MSAT && ic3_engine) {
if (se == MSAT && ic3_engine) {
// These will be managed by the solver object
// don't need to destroy
unordered_map<string, string> opts({ { "model_generation", "true" } });
Expand All @@ -162,12 +158,18 @@ SmtSolver create_solver_for(
if (logging) {
s = make_shared<LoggingSolver>(s);
}
if (printing) {
s = smt::create_printing_solver(
s, &cerr, smt::PrintingStyleEnum::MSAT_STYLE);
}
return s;
}
} else {
#endif
else {
s = create_solver(se, logging);
// no special options yet for solvers other than mathsat
s = create_solver(se, logging, true, true, printing);
#ifdef WITH_MSAT
}
#endif

assert(s);
if (ic3_engine) {
Expand Down

0 comments on commit d6a81c5

Please sign in to comment.