Commit b5ae6c9d authored by phlo's avatar phlo

fixed handling of unsat instances in Z3::solve

parent 5bbdf7fa
......@@ -97,14 +97,16 @@ std::unique_ptr<Trace> Z3::solve (Encoder & encoder)
time = runtime::measure([this, &encoder, &s, &m] {
s.from_string(formula(encoder).c_str());
if (s.check() != z3::sat)
throw std::runtime_error("formula is not sat");
m = s.get_model();
if (s.check() == z3::sat)
m = s.get_model();
});
const auto & programs = encoder.programs;
auto trace = std::make_unique<Trace>(programs, encoder.mmap);
if (!m.size())
return trace;
for (size_t step = 0; step <= encoder.bound; step++)
{
// heap state
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment