From a096cacd16844a30573066136fe525aeea4c17fe Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 29 Jan 2025 10:31:10 -0800
Subject: [PATCH] SMT: make --record_hints settable

After previous patch, this now works fine to regenerate hints for only a
few definitions, perhaps admitting the rest.
---
 src/basic/FStarC.Options.fst                  | 1 +
 src/smtencoding/FStarC.SMTEncoding.Solver.fst | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst
index 64e3b12b7c5..24d653f4a14 100644
--- a/src/basic/FStarC.Options.fst
+++ b/src/basic/FStarC.Options.fst
@@ -1745,6 +1745,7 @@ let settable = function
     | "quake"
     | "query_cache"
     | "query_stats"
+    | "record_hints"
     | "record_options"
     | "retry"
     | "reuse_hint_for"
diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst
index 58e463f911e..9fddf589fb3 100644
--- a/src/smtencoding/FStarC.SMTEncoding.Solver.fst
+++ b/src/smtencoding/FStarC.SMTEncoding.Solver.fst
@@ -1250,7 +1250,7 @@ type solver_cfg = {
   valid_intro      : bool;
   valid_elim       : bool;
   z3version        : string;
-  context_pruning  : bool
+  context_pruning  : bool;
 }
 
 let _last_cfg : ref (option solver_cfg) = BU.mk_ref None