fix merge in EncodeTerm.fsti; tweak rlimit

FStarLang · Jan 25, 2025 · 870f277 · 870f277
1 parent 4879e42
commit 870f277
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fsti b/src/smtencoding/FStarC.SMTEncoding.EncodeTerm.fsti
@@ -18,7 +18,7 @@ module FStarC.SMTEncoding.EncodeTerm
 open Prims
 open FStar.Pervasives
 open FStarC.Effect
-open FStar open FStarC
+open FStar
 open FStarC
 open FStarC.TypeChecker.Env
 open FStarC.Syntax
@@ -30,7 +30,7 @@ open FStarC.Const
 open FStarC.SMTEncoding
 open FStarC.SMTEncoding.Util
 open FStarC.SMTEncoding.Env
-module BU = FStarC.Compiler.Util
+
 val isTotFun_axioms: Range.range -> head:term -> extra_vars:fvs -> vars:fvs -> guards:list term -> bool -> term
 val mk_Apply : e:term -> vars:fvs -> term
 val maybe_curry_app : rng:Range.range -> head:either op term -> arity:int -> args:list term -> term

diff --git a/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst b/ulib/experimental/FStar.InteractiveHelpers.PostProcess.fst
@@ -597,6 +597,8 @@ let rec strip_implicit_parameters tm =
   | _ -> tm
 
 val unfold_in_assert_or_assume : bool -> exploration_result term -> Tac unit
+#push-options "--z3rlimit_factor 2 --fuel 0"
+#restart-solver
 let unfold_in_assert_or_assume dbg ares =
   print_dbg dbg ("[> unfold_in_assert_or_assume:\n" ^ term_to_string ares.res);
   (* Find the focused term inside the assert, and on which side of the
@@ -733,6 +735,7 @@ let unfold_in_assert_or_assume dbg ares =
   let ge3, asserts = subst_shadowed_with_abs_in_assertions dbg ge2 None asserts in
   (* Output *)
   printout_success ge3 asserts
+#pop-options
 
 [@plugin]
 val pp_unfold_in_assert_or_assume : bool -> unit -> Tac unit