Skip to content
Permalink
Browse files

error msg for vacuous loop check

  • Loading branch information...
scauligi committed Sep 3, 2019
1 parent 3de0124 commit 68f6939cb68b78c327936cf74ea88ab4cff851f9
Showing with 3 additions and 3 deletions.
  1. +3 −3 src/oobcheck.ml
@@ -145,15 +145,15 @@ class oobchecker debug m =
visit#_pop ()
end

method _assert_sat p zexpr =
method _assert_sat p zexpr msg =
visit#_push ();
visit#_add zexpr;
begin
match (Solver.check _solver []) with
| Solver.SATISFIABLE -> ()
| Solver.UNSATISFIABLE ->
Log.error "unsat!";
raise @@ err p
raise @@ cerr p msg
| Solver.UNKNOWN ->
print_endline "unknown!";
print_endline @@ Solver.get_reason_unknown _solver;
@@ -574,7 +574,7 @@ class oobchecker debug m =
else mk_ult,mk_ule) in
let nonvacuous_loop_check = cmp ctx zlo zhi in
let nonvacuous_loop_warn = cmpe ctx zlo zhi in
visit#_assert_sat p nonvacuous_loop_check;
visit#_assert_sat p nonvacuous_loop_check "vacuous loop";
visit#_assert_warn p nonvacuous_loop_warn "possible vacuous loop";
let zconstraint =
Boolean.mk_and ctx

0 comments on commit 68f6939

Please sign in to comment.
You can’t perform that action at this time.