From 35c6b1c3c3dbd1b782cb00206c773021f5c74765 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jun 2024 14:32:19 +0200
Subject: Add an option to run Aeneas as a borrow checker

---
 compiler/SymbolicToPure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler/SymbolicToPure.ml')

diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 848bfe50..ba6bba68 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -3693,7 +3693,7 @@ let wrap_in_match_fuel (span : Meta.span) (fuel0 : VarId.id) (fuel : VarId.id)
   let fail_branch =
     mk_result_fail_texpression_with_error_id span error_out_of_fuel_id body.ty
   in
-  match !Config.backend with
+  match Config.backend () with
   | FStar ->
       (* Generate an expression:
          {[
-- 
cgit v1.2.3