add --enum-inst option for cvc5

leanprover-community · Dec 4, 2024 · 8fc8cad · 8fc8cad
1 parent 436da90
commit 8fc8cad
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Auto/Solver/SMT.lean b/Auto/Solver/SMT.lean
@@ -108,7 +108,7 @@ def createSolver (name : SolverName) : MetaM SolverProc := do
   | .none => throwError "{decl_name%} :: Unexpected error"
   | .z3   => createAux "z3" #["-in", "-smt2", s!"-T:{tlim}"]
   | .cvc4 => throwError "cvc4 is not supported"
-  | .cvc5 => createAux "cvc5" #[s!"--tlimit={tlim * 1000}", "--produce-models"]
+  | .cvc5 => createAux "cvc5" #[s!"--tlimit={tlim * 1000}", "--produce-models", "--enum-inst"]
 where
   createAux (path : String) (args : Array String) : MetaM SolverProc :=
     IO.Process.spawn {stdin := .piped, stdout := .piped, stderr := .piped,