From 8d980ea704065123ca7c243a490502cbcfb16c38 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 28 May 2022 12:13:18 -0700
Subject: [PATCH] remove internal configuration

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 doc/mk_api_doc.py                |  1 -
 src/ast/rewriter/bv_rewriter.cpp | 21 ---------------------
 src/ast/rewriter/bv_rewriter.h   |  4 ++--
 3 files changed, 2 insertions(+), 24 deletions(-)

diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py
index 2ef219506..fd994166a 100644
--- a/doc/mk_api_doc.py
+++ b/doc/mk_api_doc.py
@@ -11,7 +11,6 @@ import getopt
 import pydoc
 import sys
 import subprocess
-import shutil
 
 ML_ENABLED=False
 MLD_ENABLED=False
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 1fdd7bd14..fe44f8fda 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -33,7 +33,6 @@ void bv_rewriter::updt_local_params(params_ref const & _p) {
     m_split_concat_eq = p.split_concat_eq();
     m_bvnot_simpl = p.bv_not_simpl();
     m_bv_sort_ac = p.bv_sort_ac();
-    m_mkbv2num = _p.get_bool("mkbv2num", false);
     m_extract_prop = p.bv_extract_prop();
     m_ite2id = p.bv_ite2id();
     m_le_extra = p.bv_le_extra();
@@ -49,9 +48,6 @@ void bv_rewriter::updt_params(params_ref const & p) {
 void bv_rewriter::get_param_descrs(param_descrs & r) {
     poly_rewriter<bv_rewriter_core>::get_param_descrs(r);
     bv_rewriter_params::collect_param_descrs(r);
-#ifndef _EXTERNAL_RELEASE
-    r.insert("mkbv2num", CPK_BOOL, "(default: false) convert (mkbv [true/false]*) into a numeral");
-#endif
 }
 
 br_status bv_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@@ -2723,23 +2719,6 @@ br_status bv_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result) {
 
 
 br_status bv_rewriter::mk_mkbv(unsigned num, expr * const * args, expr_ref & result) {
-    if (m_mkbv2num) {
-        unsigned i;
-        for (i = 0; i < num; i++)
-            if (!m().is_true(args[i]) && !m().is_false(args[i]))
-                return BR_FAILED;
-        numeral val;
-        numeral two(2);
-        i = num;
-        while (i > 0) {
-            --i;
-            val *= two;
-            if (m().is_true(args[i]))
-                val++;
-        }
-        result = mk_numeral(val, num);
-        return BR_DONE;
-    }
     return BR_FAILED;
 }
 
diff --git a/src/ast/rewriter/bv_rewriter.h b/src/ast/rewriter/bv_rewriter.h
index 88d952c06..23ae67277 100644
--- a/src/ast/rewriter/bv_rewriter.h
+++ b/src/ast/rewriter/bv_rewriter.h
@@ -55,7 +55,6 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_mul2concat;
     bool       m_bit2bool;
     bool       m_blast_eq_value;
-    bool       m_mkbv2num;
     bool       m_ite2id;
     bool       m_split_concat_eq;
     bool       m_bv_sort_ac;
@@ -63,7 +62,8 @@ class bv_rewriter : public poly_rewriter<bv_rewriter_core> {
     bool       m_bvnot_simpl;
     bool       m_le_extra;
     bool       m_le2extract;
-
+    bool       m_mkbv2num = false;
+    
     bool is_zero_bit(expr * x, unsigned idx);
 
     br_status mk_ule(expr * a, expr * b, expr_ref & result);