From 54e493eaede8907496487e41070347fa0d0b22c9 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 21 Jan 2022 11:09:11 +0100
Subject: Make minor modifications for the invariants checks

---
 src/InterpreterStatements.ml | 12 ++----------
 src/Invariants.ml            | 11 +++++++----
 2 files changed, 9 insertions(+), 14 deletions(-)

diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index edc3bef1..d76def43 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -714,10 +714,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
    * checking the invariants *)
   let cc = greedy_expand_symbolic_values config in
   (* Sanity check *)
-  let cc =
-    if config.C.check_invariants then comp cc (Inv.cf_check_invariants config)
-    else cc
-  in
+  let cc = comp cc (Inv.cf_check_invariants config) in
 
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
@@ -1160,12 +1157,7 @@ and eval_function_body (config : C.config) (body : A.statement) : st_cm_fun =
      * checking the invariants *)
     let cc = greedy_expand_symbolic_values config in
     (* Sanity check *)
-    let cc =
-      if config.C.check_invariants then
-        comp_check_ctx cc (Inv.check_invariants config)
-      else cc
-    in
-
+    let cc = comp_check_ctx cc (Inv.check_invariants config) in
     (* Continue *)
     cc (cf res)
   in
diff --git a/src/Invariants.ml b/src/Invariants.ml
index 5e114c19..b16e71d0 100644
--- a/src/Invariants.ml
+++ b/src/Invariants.ml
@@ -766,10 +766,13 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit =
   M.iter check_info !infos
 
 let check_invariants (config : C.config) (ctx : C.eval_ctx) : unit =
-  check_loans_borrows_relation_invariant ctx;
-  check_borrowed_values_invariant ctx;
-  check_typing_invariant ctx;
-  check_symbolic_values config ctx
+  if config.C.check_invariants then (
+    log#ldebug (lazy "Checking invariants");
+    check_loans_borrows_relation_invariant ctx;
+    check_borrowed_values_invariant ctx;
+    check_typing_invariant ctx;
+    check_symbolic_values config ctx)
+  else log#ldebug (lazy "Not checking invariants (check is not activated)")
 
 (** Same as [check_invariants], but written in CPS *)
 let cf_check_invariants (config : C.config) : cm_fun =
-- 
cgit v1.2.3