mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-03 13:56:08 +00:00
Code Activity

Fix OCaml build error: use status instead of solver_result in z3.mli

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-20 04:32:56 +00:00
parent 5253f9af9d
commit ce0fb1bd24
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/ml/z3.mli
View file

@ -3439,7 +3439,7 @@ sig
(** Retrieve fixed assignments to variables as consequences given assumptions. (** Retrieve fixed assignments to variables as consequences given assumptions.
Returns the solver status and a list of consequence expressions. Returns the solver status and a list of consequence expressions.
Each consequence is an implication: assumptions => variable = value. *) Each consequence is an implication: assumptions => variable = value. *)
val get_consequences : solver -> Expr.expr list -> Expr.expr list -> solver_result * Expr.expr list val get_consequences : solver -> Expr.expr list -> Expr.expr list -> status * Expr.expr list
(** Solve constraints treating given variables symbolically. (** Solve constraints treating given variables symbolically.
variables are the variables to solve for, terms are the substitution terms, variables are the variables to solve for, terms are the substitution terms,