Make fpa2bv debug symbol names optional

Z3Prover · Oct 12, 2021 · f1acc4b · f1acc4b
1 parent 515a2a7
commit f1acc4b
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 7 deletions.
diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp
@@ -346,7 +346,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
         app * a0 = to_app(val->get_arg(0));
 
         expr_ref v0(m), v1(m), v2(m);
-#ifdef Z3DEBUG
+#ifdef Z3DEBUG_FPA2BV_NAMES
         app * a1 = to_app(val->get_arg(1));
         app * a2 = to_app(val->get_arg(2));
         v0 = mc->get_const_interp(a0->get_decl());
@@ -378,17 +378,18 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
 
         SASSERT(val->is_app_of(m_fpa_util.get_family_id(), OP_FPA_FP));
 
-#ifdef Z3DEBUG
+#ifdef Z3DEBUG_FPA2BV_NAMES
         SASSERT(to_app(val->get_arg(0))->get_decl()->get_arity() == 0);
         SASSERT(to_app(val->get_arg(1))->get_decl()->get_arity() == 0);
         SASSERT(to_app(val->get_arg(2))->get_decl()->get_arity() == 0);
         seen.insert(to_app(val->get_arg(0))->get_decl());
         seen.insert(to_app(val->get_arg(1))->get_decl());
         seen.insert(to_app(val->get_arg(2))->get_decl());
 #else
-        SASSERT(a->get_arg(0)->get_kind() == OP_EXTRACT);
-        SASSERT(to_app(a->get_arg(0))->get_arg(0)->get_kind() == OP_EXTRACT);
+        SASSERT(is_app(val->get_arg(0)));
+        SASSERT(m_bv_util.is_extract(val->get_arg(0)));
         seen.insert(to_app(to_app(val->get_arg(0))->get_arg(0))->get_decl());
+
 #endif
 
         if (!sgn && !sig && !exp)

diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
@@ -192,7 +192,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
 
         app_ref sgn(m), s(m), e(m);
 
-#ifdef Z3DEBUG
+#ifdef Z3DEBUG_FPA2BV_NAMES
         std::string p("fpa2bv");
         std::string name = f->get_name().str();
 
@@ -326,7 +326,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
 
         expr_ref bv3(m);
         bv3 = m.mk_fresh_const(
-#ifdef Z3DEBUG
+#ifdef Z3DEBUG_FPA2BV_NAMES
             "fpa2bv_rm"
 #else
             nullptr
@@ -3839,7 +3839,7 @@ void fpa2bv_converter::mk_rounding_mode(decl_kind k, expr_ref & result)
 }
 
 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {
-#ifdef Z3DEBUG
+#ifdef Z3DEBUG_FPA2BV_NAMES
     return;
     // CMW: This works only for quantifier-free formulas.
     if (m_util.is_fp(e)) {