allow use_hints even when context_pruning is set

FStarLang · Jan 30, 2025 · 13a2b89 · 13a2b89
1 parent 0fe5acd
commit 13a2b89
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.fst
@@ -65,7 +65,7 @@ let replaying_hints: ref (option hints) = BU.mk_ref None
 (****************************************************************************)
 (* Hint databases (public)                                                  *)
 (****************************************************************************)
-let use_hints () = Options.use_hints () && Options.Ext.get "context_pruning" = ""
+let use_hints () = Options.use_hints ()
 let initialize_hints_db src_filename format_filename : unit =
     if Options.record_hints() then recorded_hints := Some [];
     let norm_src_filename = BU.normalize_file_path src_filename in