diff mbox series

[6/8] scheck: allow multiple assertions

Message ID 20210410133045.53189-7-luc.vanoostenryck@gmail.com (mailing list archive)
State Superseded, archived
Headers show
Series scheck: add a symbolic checker for sparse | expand

Commit Message

Luc Van Oostenryck April 10, 2021, 1:30 p.m. UTC 
With the SMT solver used here, by default, once an expression is
checked it's kinda consumed by the process and can't be reused
anymore for another check.

So, enable the incremental mode: it allows to call boolecter_sat()
several times.

Note: Another would be, of course, to just AND together all assertions
      and just check this but then we would lost the finer grained
      diagnostic in case of failure.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>
---
 scheck.c               | 5 +++--
 validation/scheck/ok.c | 4 ----
 2 files changed, 3 insertions(+), 6 deletions(-)
diff mbox series

Patch

diff --git a/scheck.c b/scheck.c
index ff91328f681a..26f88a4a028e 100644
--- a/scheck.c
+++ b/scheck.c
@@ -241,6 +241,7 @@  static bool check_function(struct entrypoint *ep)
 	int rc = 0;
 
 	boolector_set_opt(btor, BTOR_OPT_MODEL_GEN, 1);
+	boolector_set_opt(btor, BTOR_OPT_INCREMENTAL, 1);
 
 	FOR_EACH_PTR(ep->bbs, bb) {
 		struct instruction *insn;
@@ -261,8 +262,8 @@  static bool check_function(struct entrypoint *ep)
 				ternop(btor, insn);
 				break;
 			case OP_CALL:
-				rc = check_call(btor, insn);
-				goto out;
+				rc &= check_call(btor, insn);
+				break;
 			case OP_RET:
 				goto out;
 			default:
diff --git a/validation/scheck/ok.c b/validation/scheck/ok.c
index 76c04c4f6870..f4a0daabfe9a 100644
--- a/validation/scheck/ok.c
+++ b/validation/scheck/ok.c
@@ -1,10 +1,6 @@ 
 static void ok(int x)
 {
 	__assert((~x) == (~0 - x));	// true but not simplified yet
-}
-
-static void also_ok(int x)
-{
 	__assert_eq(~x, ~0 - x);
 }