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)