Module Z3backend.Io

val init_backend : unit -> unit
type backend_context
val make_context : Shared_ast.decl_ctx -> backend_context
type vc_encoding
type model
type vc_encoding_result =
| Success of vc_encoding * backend_context
| Fail of string
val print_negative_result : Conditions.verification_condition -> backend_context -> model option -> string

encode_and_check_vc spawns a new Z3 solver and tries to solve the expression vc. Returns true if the vs was proven true and false otherwise. *