From d11556aece9f6518455c231beae6308164870022 Mon Sep 17 00:00:00 2001
From: Louis Gesbert <louis.gesbert@ocamlpro.com>
Date: Mon, 8 Nov 2021 12:30:57 +0100
Subject: [PATCH] Update changes, comment out z3 debugging code

---
 master_changes.md                |  1 +
 src/solver/opamBuiltinZ3.real.ml | 12 ++++++------
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/master_changes.md b/master_changes.md
index 1af4b867766..9a887b79af5 100644
--- a/master_changes.md
+++ b/master_changes.md
@@ -129,6 +129,7 @@ users)
 ## Solver
   * [BUG] Remove z3 debug output [#4723 @rjbou - fix #4717] [2.1.0~rc2 #4720]
   * Fix and improve the Z3 solver backend [#4880 @altgr]
+  * Refactored, fixed, improved and optimised the z3 solver backend [#4878 @altgr]
 
 ## Client
   *
diff --git a/src/solver/opamBuiltinZ3.real.ml b/src/solver/opamBuiltinZ3.real.ml
index f64456ab856..f85576d1496 100644
--- a/src/solver/opamBuiltinZ3.real.ml
+++ b/src/solver/opamBuiltinZ3.real.ml
@@ -501,12 +501,12 @@ let call ~criteria ?timeout (preamble, universe, _ as cudf) =
   Z3.Optimize.add opt ctx.constr_defs;
   Z3.Optimize.add opt request_def;
   log "Resolving...";
-  (match Sys.getenv "OPAMZ3DEBUG" with
-   | exception Not_found -> ()
-   | f ->
-     let debug = open_out (f^".smt2") in
-     output_string debug (Z3.Optimize.to_string opt);
-     close_out debug);
+  (* (match Sys.getenv "OPAMZ3DEBUG" with
+   *  | exception Not_found -> ()
+   *  | f ->
+   *    let debug = open_out (f^".smt2") in
+   *    output_string debug (Z3.Optimize.to_string opt);
+   *    close_out debug); *)
   match Z3.Optimize.check opt with
   | UNSATISFIABLE ->
     log "UNSAT";