From ce033a8e3654ba1f9be06b9bab8202cc5a7d5b2b Mon Sep 17 00:00:00 2001 From: Alberto Gonzalez Date: Wed, 1 Apr 2020 19:32:44 +0000 Subject: Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`. --- passes/sat/qbfsat.cc | 2 ++ 1 file changed, 2 insertions(+) (limited to 'passes/sat/qbfsat.cc') diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 833cab167..a16ee546f 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -507,6 +507,8 @@ struct QbfSatPass : public Pass { } else if (!ret.unknown && !ret.sat && opt.sat) log_cmd_error("expected problem to be SAT\n"); + else if (ret.unknown && (opt.sat || opt.unsat)) + log_cmd_error("expected problem to be %s\n", opt.sat? "SAT" : "UNSAT"); } else { specialize_from_file(module, opt.specialize_soln_file); Pass::call(design, "opt_clean"); -- cgit v1.2.3