From fb6c18763fe33401bcdd352d9e4d9934f8a4fa6e Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 16 Mar 2022 11:20:20 +0100 Subject: [PATCH] Fix encoding of hypotheses into Z3 --- compiler/verification/io.ml | 2 +- compiler/verification/z3backend.real.ml | 11 ++++++----- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/compiler/verification/io.ml b/compiler/verification/io.ml index 7b70c021..ad32e528 100644 --- a/compiler/verification/io.ml +++ b/compiler/verification/io.ml @@ -171,7 +171,7 @@ module MakeBackendIO (B : Backend) = struct match z3_vc with | Success (encoding, backend_ctx) -> ( - Cli.debug_print "The translation to Z3 is the following:@\n%s" + Cli.debug_print "The translation to Z3 is the following:\n%s" (B.print_encoding encoding); match B.solve_vc_encoding backend_ctx encoding with | ProvenTrue -> Cli.result_print "%s" (print_positive_result vc) diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 6ec9b141..68d18426 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -777,11 +777,12 @@ module Backend = struct let solve_vc_encoding (ctx : backend_context) (encoding : vc_encoding) : solver_result = let solver = Z3.Solver.mk_solver ctx.ctx_z3 None in - (* Add all the constraints stored in the context *) - let encoding = - Boolean.mk_and ctx.ctx_z3 (encoding :: ctx.ctx_z3constraints) - in - Z3.Solver.add solver [ Boolean.mk_not ctx.ctx_z3 encoding ]; + (* We take the negation of the query to check for possible + counterexamples *) + let query = Boolean.mk_not ctx.ctx_z3 encoding in + (* Add all the hypotheses stored in the context *) + let query_and_hyps = query :: ctx.ctx_z3constraints in + Z3.Solver.add solver query_and_hyps; match Z3.Solver.check solver [] with | UNSATISFIABLE -> ProvenTrue | SATISFIABLE -> ProvenFalse (Z3.Solver.get_model solver)