SMT: remove ill-typed unused definition

FStarLang · Nov 30, 2023 · 475518f · 475518f
1 parent cffd0ac
commit 475518f
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst
@@ -48,10 +48,6 @@ exception SplitQueryAndRetry
 // The type definition is now in [FStar.Compiler.Util], since it needs to be visible to
 // both the F# and OCaml implementations.
 
-type z3_replay_result = either Z3.unsat_core, error_labels
-let z3_result_as_replay_result = function
-    | Inl l -> Inl l
-    | Inr (r, _) -> Inr r
 let recorded_hints : ref (option hints) = BU.mk_ref None
 let replaying_hints: ref (option hints) = BU.mk_ref None