Merge pull request #3562 from mtzguido/cache

Fix some missing branches for ShowOptions
FStarLang · Oct 14, 2024 · 20e0256 · 20e0256
2 parents ba3ae57 + 0dcc1e1
commit 20e0256
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 12 deletions.
diff --git a/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml b/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml
diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml
diff --git a/src/parser/FStarC.Parser.AST.Util.fst b/src/parser/FStarC.Parser.AST.Util.fst
@@ -462,6 +462,7 @@ let eq_lift (t1 t2: lift) =
 
 let eq_pragma (t1 t2: pragma) =
   match t1, t2 with
+  | ShowOptions, ShowOptions -> true
   | SetOptions s1, SetOptions s2 -> s1 = s2
   | ResetOptions s1, ResetOptions s2 -> eq_option (fun s1 s2 -> s1 = s2) s1 s2
   | PushOptions s1, PushOptions s2 -> eq_option (fun s1 s2 -> s1 = s2) s1 s2

diff --git a/src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst b/src/smtencoding/FStarC.SMTEncoding.Solver.Cache.fst
@@ -65,12 +65,13 @@ instance hashable_letbinding : hashable letbinding = {
 
 instance hashable_pragma : hashable pragma = {
   hash = (function
-          | SetOptions s -> hash 1 `mix` hash s
-          | ResetOptions s -> hash 2 `mix` hash s
-          | PushOptions s -> hash 3 `mix` hash s
-          | PopOptions -> hash 4
-          | RestartSolver -> hash 5
-          | PrintEffectsGraph -> hash 6);
+          | ShowOptions -> hash 1
+          | SetOptions s -> hash 2 `mix` hash s
+          | ResetOptions s -> hash 3 `mix` hash s
+          | PushOptions s -> hash 4 `mix` hash s
+          | PopOptions -> hash 5
+          | RestartSolver -> hash 6
+          | PrintEffectsGraph -> hash 7);
 }
 
 let rec hash_sigelt (se:sigelt) : hash_code =