summaryrefslogtreecommitdiff
path: root/passes
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-06-23 13:28:30 +0200
committerClifford Wolf <clifford@clifford.at>2013-06-23 13:28:30 +0200
commit101491132fbd617b0a0819045cc7b5d35395706d (patch)
tree2373089242627eda25550aaf98cda08385bee5d9 /passes
parent46b177eb8a7a9e52eee4fd2e4a86c56f9a1fb44a (diff)
Added SAT support for -all/-max with -verify
Diffstat (limited to 'passes')
-rw-r--r--passes/sat/sat.cc17
1 files changed, 11 insertions, 6 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index 769d94a0..c7520423 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -659,7 +659,7 @@ struct SatPass : public Pass {
}
else
{
- if (loopcount > 0)
+ if (maxsteps > 0)
log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
SatHelper sathelper(design, module);
@@ -702,16 +702,16 @@ struct SatPass : public Pass {
sathelper.print_model();
- if (verify) {
- log("\n");
- log_error("Called with -verify and proof did fail!\n");
- }
-
if (loopcount != 0) {
loopcount--, did_rerun = true;
sathelper.invalidate_model();
goto rerun_solver;
}
+
+ if (verify) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
}
else
{
@@ -726,6 +726,11 @@ struct SatPass : public Pass {
print_qed();
}
}
+
+ if (verify && did_rerun) {
+ log("\n");
+ log_error("Called with -verify and proof did fail!\n");
+ }
}
if (0) {