From 1c7c1bb9fac25dda0fb0412b33227299ccfdd3f0 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 10 Feb 2022 10:00:15 +0100
Subject: Add an option to deactivate the invariant checks

---
 src/main.ml | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'src/main.ml')

diff --git a/src/main.ml b/src/main.ml
index cf854577..4a111a25 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -33,6 +33,7 @@ let () =
   let no_decreases_clauses = ref false in
   let template_decreases_clauses = ref false in
   let no_split = ref false in
+  let no_check_inv = ref false in
 
   let spec =
     [
@@ -63,20 +64,23 @@ let () =
       ( "-test-trans-units",
         Arg.Set test_trans_units,
         " Test the translated unit functions with the target theorem\n\
-        \                        prover's normalizer" );
+        \                         prover's normalizer" );
       ( "-no-decreases-clauses",
         Arg.Set no_decreases_clauses,
         " Do not add decrease clauses to the recursive definitions" );
       ( "-template-clauses",
         Arg.Set template_decreases_clauses,
         " Generate templates for the required decreases clauses, in a\n\
-         `\n\
-        \                                dedicated file. Incompatible with \
+        \                         dedicated file. Incompatible with \
          -no-decreases-clauses" );
       ( "-no-split",
         Arg.Set no_split,
-        " Don't split the definitions between different files for types, \
-         functions, etc." );
+        " Don't split the definitions between different files for types,\n\
+        \                         functions, etc." );
+      ( "-no-check-inv",
+        Arg.Set no_check_inv,
+        " Deactivate the invariant sanity checks performed at every step of\n\
+        \                         evaluation. Dramatically saves speed." );
     ]
   in
   (* Sanity check: -template-clauses ==> not -no-decrease-clauses *)
@@ -146,7 +150,7 @@ let () =
       (* Some options for the execution *)
       let eval_config =
         {
-          C.check_invariants = true;
+          C.check_invariants = not !no_check_inv;
           greedy_expand_symbolics_with_borrows = true;
           allow_bottom_below_borrow = true;
         }
-- 
cgit v1.2.3