diff options
| -rw-r--r-- | scheck.c | 5 | ||||
| -rw-r--r-- | validation/scheck/ok.c | 4 |
2 files changed, 3 insertions, 6 deletions
@@ -252,6 +252,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; @@ -274,8 +275,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 76c04c4f..f4a0daab 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); } |