simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 03:05:31 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

better error

Browse source
This commit is contained in:
Simon Cruanes 2022-10-19 22:29:13 -04:00
parent cc090a4574
commit 082bfdd43a
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smtlib/build_model.ml
View file

@ -29,10 +29,10 @@ let build (self : t) (sat : Solver.sat_result) : Model.t =
(fun v' -> (fun v' ->
if not (Term.equal value v') then if not (Term.equal value v') then
Error.errorf Error.errorf
"Inconsistent model@ for fun `%a`,@ values %a@ map to `%a` and \ "Inconsistent model@ for fun `%a`,@ arguments %a@ map to `%a` \
`%a`" and `%a` (already existing binding)@ found from term `%a`"
Term.pp f (Fmt.Dump.list Term.pp) v_args Term.pp value Term.pp Term.pp f (Fmt.Dump.list Term.pp) v_args Term.pp value Term.pp
v') v' Term.pp t)
other_v; other_v;
(* save mapping *) (* save mapping *)
m := Model.add_fun_entry f v_args value !m m := Model.add_fun_entry f v_args value !m