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

[skip ci] Z3encoding: obtain type of bound variables

Browse Source
This commit is contained in:
Aymeric Fromherz 2022-01-12 15:58:19 +01:00
parent c7b225bad5
commit d455e29978
1 changed files with 9 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
compiler/verification/z3encoding.ml
View File

@ -227,7 +227,15 @@ let solve_vc (prgm : program) (decl_ctx : decl_ctx) (vcs : Conditions.verificati
try
Success
(translate_expr
{ ctx_z3 = z3_ctx; ctx_decl = decl_ctx; ctx_var = variable_types prgm }
{
ctx_z3 = z3_ctx;
ctx_decl = decl_ctx;
ctx_var =
VarMap.union
(fun _ _ _ ->
failwith "[Z3 encoding]: A Variable cannot be both free and bound")
(variable_types prgm) vc.Conditions.vc_free_vars_typ;
}
vc.Conditions.vc_guard)
with Failure msg -> Fail msg ))
vcs