mirror of https://github.com/YosysHQ/yosys.git
Fix handling of `-sat` and `-unsat` options when the solver returns `unknown`.
This commit is contained in:
parent
6af8b767b4
commit
ce033a8e36
|
@ -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");
|
||||
|
|
Loading…
Reference in New Issue