Found against strata-org/Strata at a61d47e5643820dc08a7d119d3226df48d20926b, while building the repository and running the deductive verifier on macOS 15.7.3 arm64 with Lean 4.29.1, cvc5 1.3.4 and z3 4.15.2.
Files written by --vc-directory end with (get-value ...) but do not set (set-option :produce-models true), so replaying one with the default solver fails: cvc5 /tmp/vcdir/cap_holds_0.smt2 prints sat and then (error "cannot get value unless model generation is enabled (try --produce-models)"). The tool itself is unaffected, because getSolverFlags at Strata/Languages/Core/Verifier.lean:533-545 passes --produce-models for cvc5 on the command line, and z3 answers the same file without complaint because it does not need the option. The cost falls on anyone handing a dumped VC to a solver by hand or to a colleague, which is most of what a VC dump is for. Suggested modification: emit (set-option :produce-models true) into the file alongside the (get-value ...), so the artifact is self-contained. Worth deciding whether the dump is meant to be replayable, since if it is not then documenting the required flag would do instead.
Found against
strata-org/Strataata61d47e5643820dc08a7d119d3226df48d20926b, while building the repository and running the deductive verifier on macOS 15.7.3 arm64 with Lean 4.29.1, cvc5 1.3.4 and z3 4.15.2.Files written by
--vc-directoryend with(get-value ...)but do not set(set-option :produce-models true), so replaying one with the default solver fails:cvc5 /tmp/vcdir/cap_holds_0.smt2printssatand then(error "cannot get value unless model generation is enabled (try --produce-models)"). The tool itself is unaffected, becausegetSolverFlagsatStrata/Languages/Core/Verifier.lean:533-545passes--produce-modelsfor cvc5 on the command line, and z3 answers the same file without complaint because it does not need the option. The cost falls on anyone handing a dumped VC to a solver by hand or to a colleague, which is most of what a VC dump is for. Suggested modification: emit(set-option :produce-models true)into the file alongside the(get-value ...), so the artifact is self-contained. Worth deciding whether the dump is meant to be replayable, since if it is not then documenting the required flag would do instead.