From 412bf9bd2ed8ae57eb8a295c0eb5e473af3cf86c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Tue, 28 Jan 2025 08:45:29 -0800 Subject: [PATCH] SMT: introduce --ext fast_hints: only set produce-unsat-cores when recording hints --- src/smtencoding/FStarC.SMTEncoding.Z3.fst | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/smtencoding/FStarC.SMTEncoding.Z3.fst b/src/smtencoding/FStarC.SMTEncoding.Z3.fst index c2a65d2b36f..e41e11f2900 100644 --- a/src/smtencoding/FStarC.SMTEncoding.Z3.fst +++ b/src/smtencoding/FStarC.SMTEncoding.Z3.fst @@ -552,7 +552,6 @@ let z3_options (ver:string) = "(set-option :global-decls false)"; "(set-option :smt.mbqi false)"; "(set-option :auto_config false)"; - "(set-option :produce-unsat-cores true)"; "(set-option :model true)"; "(set-option :smt.case_split 3)"; "(set-option :smt.relevancy 2)"; @@ -614,6 +613,13 @@ let mk_input (fresh : bool) (theory : list decl) : string & option string & opti ) :: theory in let options = z3_options ver in + let options = + (* With --ext fast_hints, we only enable unsat-core generation + if we are actually recording hints. *) + if Options.Ext.enabled "fast_hints" && not (Options.record_hints ()) + then options + else options ^ "(set-option :produce-unsat-cores true)\n" + in let options = options ^ (Options.z3_smtopt() |> String.concat "\n") ^ "\n\n" in if Options.print_z3_statistics() then context_profile theory; let r, hash =