Start working on greedy symbolic value expansion and expansion before

assignment

1 files changed, 10 insertions, 2 deletions

diff --git a/src/main.ml b/src/main.ml
index c6545fcb..e8f46b99 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -59,8 +59,16 @@ let () =
       (* Print the module *)
       main_log#ldebug (lazy ("\n" ^ Print.Module.module_to_string m ^ "\n"));
 
+      (* Some options for the execution *)
+      let config =
+        {
+          C.check_invariants = true;
+          greedy_expand_symbolics_with_borrows = false;
+        }
+      in
+
       (* Test the unit functions with the concrete interpreter *)
-      I.Test.test_unit_functions m.types m.functions;
+      I.Test.test_unit_functions config m;
 
       (* Evaluate the symbolic interpreter on the functions *)
-      I.Test.test_functions_symbolic m.types m.functions
+      I.Test.test_functions_symbolic config m