CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 16:28:12 +03:00
Code Issues Projects Releases Wiki Activity

[Z3encoding] Print variable name when encoding is not supported

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-03-15 18:02:08 +01:00
parent ecdd3dfaef
commit d760d883a6
2 changed files with 9 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
compiler/lcalc/ast.ml
View File

@ -134,7 +134,9 @@ let make_matchopt_with_abs_arms
(e_some : expr Pos.marked Bindlib.box) : expr Pos.marked Bindlib.box =
let pos = Pos.get_position @@ Bindlib.unbox arg in
let mark : 'a -> 'a Pos.marked = Pos.mark pos in
let+ arg = arg and+ e_none = e_none and+ e_some = e_some [@ocamlformat "disable"] in
let+ arg = arg
and+ e_none = e_none
and+ e_some = e_some [@ocamlformat "disable"] in
mark @@ EMatch (arg, [ e_none; e_some ], option_enum)

7
compiler/verification/io.ml
View File

@ -179,5 +179,10 @@ module MakeBackendIO (B : Backend) = struct
Cli.error_print "%s" (print_negative_result vc backend_ctx model)
| Unknown ->
failwith "The solver failed at proving or disproving the VC")
| Fail msg -> Cli.error_print "The translation to Z3 failed:@\n%s" msg
| Fail msg ->
Cli.error_print "%s The translation to Z3 failed:\n%s"
(Cli.with_style [ ANSITerminal.yellow ] "[%s.%s]"
(Format.asprintf "%a" ScopeName.format_t vc.vc_scope)
(Bindlib.name_of (Pos.unmark vc.vc_variable)))
msg
end