Merge branch 'master' into twal/generalize_move_requires

FStarLang · Sep 7, 2024 · fbface2 · fbface2
2 parents e658256 + c648e62
commit fbface2
Show file tree

Hide file tree

Showing 5 changed files with 1,115 additions and 1,436 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst
@@ -1327,7 +1327,7 @@ let do_solve (can_split:bool) (is_retry:bool) use_env_msg tcenv q : unit =
   | None -> () (* already logged an error *)
 
 let split_and_solve (retrying:bool) use_env_msg tcenv q : unit =
-  if Options.query_stats () then begin
+  if Debug.any () || Options.query_stats () then begin
     let range = "(" ^ (Range.string_of_range (Env.get_range tcenv)) ^ ")" in
     BU.print2 "%s\tQuery-stats splitting query because %s\n"
                 range