SMT: make --record_hints settable

After previous patch, this now works fine to regenerate hints for only a few definitions, perhaps admitting the rest.
FStarLang · Jan 30, 2025 · a096cac · a096cac
1 parent 8104f1b
commit a096cac
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -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