Skip to content

Commit e8a0d65

Browse files
Satcheck need not implement hardness_collectort
Otherwise compilation fails for SAT solvers that don't implement hardness_collectort yet, e.g. Glucose.
1 parent 240a30a commit e8a0d65

File tree

1 file changed

+9
-5
lines changed

1 file changed

+9
-5
lines changed

src/goto-checker/solver_factory.cpp

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -178,12 +178,16 @@ static std::unique_ptr<SatcheckT>
178178
make_satcheck_prop(message_handlert &message_handler, const optionst &options)
179179
{
180180
auto satcheck = util_make_unique<SatcheckT>(message_handler);
181-
if(options.is_set("write-solver-stats-to"))
181+
if(auto hardness_collector = dynamic_cast<hardness_collectort *>(&*satcheck))
182182
{
183-
satcheck->enable_hardness_collection();
184-
satcheck->with_solver_hardness([&options](solver_hardnesst &hardness) {
185-
hardness.set_outfile(options.get_option("write-solver-stats-to"));
186-
});
183+
if(options.is_set("write-solver-stats-to"))
184+
{
185+
hardness_collector->enable_hardness_collection();
186+
hardness_collector->with_solver_hardness(
187+
[&options](solver_hardnesst &hardness) {
188+
hardness.set_outfile(options.get_option("write-solver-stats-to"));
189+
});
190+
}
187191
}
188192
return satcheck;
189193
}

0 commit comments

Comments
 (0)