From 40f7f5d00a9afff27f1d2329ab525705e57c6d6f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 19 Dec 2018 20:18:04 +0000
Subject: Improve sizeof rewriting performance

Simply constraints further before calling Z3 to improve performance of
sizeof re-writing.
---
 src/constraint.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src/constraint.ml')

diff --git a/src/constraint.ml b/src/constraint.ml
index 7ead0cc8..b00c0a4e 100644
--- a/src/constraint.ml
+++ b/src/constraint.ml
@@ -53,6 +53,8 @@ open Ast
 open Ast_util
 open Util
 
+let opt_smt_verbose = ref false
+
 (* SMTLIB v2.0 format is based on S-expressions so we have a
    lightweight representation of those here. *)
 type sexpr = List of (sexpr list) | Atom of string
@@ -185,7 +187,9 @@ let call_z3' l vars constraints : smt_result =
   let problems = [constraints] in
   let z3_file = smtlib_of_constraints l vars constraints in
 
-  (* prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file); *)
+  if !opt_smt_verbose then
+    prerr_endline (Printf.sprintf "SMTLIB2 constraints are: \n%s%!" z3_file)
+  else ();
 
   let rec input_lines chan = function
     | 0 -> []
-- 
cgit v1.2.3