From 52df2224e94de0842281899449a58966698450f5 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 16 Sep 2015 18:04:26 +0100
Subject: [PATCH] Disabled FP debug variables.
---
src/ast/fpa/fpa2bv_converter.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index af1ba8004..906327ecc 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -3323,7 +3323,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
#ifdef Z3DEBUG
- // return;
+ return;
// CMW: This works only for quantifier-free formulas.
expr_ref new_e(m);
new_e = m.mk_fresh_const(prefix, m.get_sort(e));