From fdb8555cf6bc21ea230141373920196b078bdd28 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 27 Nov 2023 13:48:46 +0100
Subject: Do not activate the sanity (invariant) checks by default

---
 Makefile | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index e0367d73..88cb7d05 100644
--- a/Makefile
+++ b/Makefile
@@ -30,11 +30,8 @@ CHARON_TESTS_POLONIUS_DIR ?= $(CHARON_HOME)/tests-polonius
 AENEAS_EXE ?= bin/aeneas
 
 # The user can specify additional translation options for Aeneas.
-# By default we do:
-# - unfold all the monadic let bindings to matches (required by F*)
-# - insert calls to the normalizer in the translated code to test the
-#   generated unit functions
-OPTIONS +=
+# By default we activate the (expensive) sanity checks.
+OPTIONS ?= -checks
 
 #
 # The rules use (and update) the following variables
-- 
cgit v1.2.3