Skip to content

Commit 86a6b58

Browse files
committed
Fix cvc5's bindings
1 parent acd3e7c commit 86a6b58

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/smtml/cvc5_mappings.default.ml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -423,7 +423,8 @@ module Fresh_cvc5 () = struct
423423
let get_symbols _ =
424424
Fmt.failwith "Cvc5_mappings: get_symbols not implemented"
425425

426-
let eval ?completion:_ solver term = Some (Solver.get_value solver term)
426+
let eval ?ctx:_ ?completion:_ solver term =
427+
Some (Solver.get_value solver term)
427428
end
428429

429430
module Solver = struct
@@ -434,7 +435,7 @@ module Fresh_cvc5 () = struct
434435
| Unsat_core ->
435436
Solver.set_option slv "produce-unsat-cores" (string_of_bool v)
436437
| Ematching -> Solver.set_option slv "e-matching" (string_of_bool v)
437-
| Parallel | Num_threads -> ()
438+
| Parallel | Num_threads | Debug -> ()
438439

439440
let set_params slv params =
440441
List.iter

0 commit comments

Comments
 (0)