diff options
Diffstat (limited to 'src/preprocessing/passes/bv_to_int.cpp')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp index c5f24c15c..28dcc1949 100644 --- a/src/preprocessing/passes/bv_to_int.cpp +++ b/src/preprocessing/passes/bv_to_int.cpp @@ -25,6 +25,7 @@ #include "expr/node.h" #include "expr/node_traversal.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" #include "options/uf_options.h" #include "preprocessing/assertion_pipeline.h" @@ -702,6 +703,7 @@ Node BVToInt::translateWithChildren(Node original, Node BVToInt::translateNoChildren(Node original) { + SkolemManager* sm = d_nm->getSkolemManager(); Node translation; Assert(original.isVar() || original.isConst()); if (original.isVar()) @@ -722,11 +724,11 @@ Node BVToInt::translateNoChildren(Node original) // New integer variables that are not bound (symbolic constants) // are added together with range constraints induced by the // bit-width of the original bit-vector variables. - Node newVar = d_nm->mkSkolem("__bvToInt_var", - d_nm->integerType(), - "Variable introduced in bvToInt " - "pass instead of original variable " - + original.toString()); + Node newVar = sm->mkDummySkolem("__bvToInt_var", + d_nm->integerType(), + "Variable introduced in bvToInt " + "pass instead of original variable " + + original.toString()); uint64_t bvsize = original.getType().getBitVectorSize(); translation = newVar; d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize)); @@ -783,9 +785,10 @@ Node BVToInt::translateFunctionSymbol(Node bvUF) { intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d); } + SkolemManager* sm = d_nm->getSkolemManager(); ostringstream os; os << "__bvToInt_fun_" << bvUF << "_int"; - intUF = d_nm->mkSkolem( + intUF = sm->mkDummySkolem( os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function"); // introduce a `define-fun` in the smt-engine to keep // the correspondence between the original |