diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-11 08:47:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-11 08:47:02 -0700 |
| commit | 1e0ff61c96c455287fd7986ce353dc2754f85d4f (patch) | |
| tree | c7ed06c967361829a9c01c02389cd1cadb2a60c8 /src/preprocessing/passes | |
| parent | 5e2366d542e17ba5064a56f2581ada99c0046ddc (diff) | |
Fix ackermannize preprocessing pass. (#1904)
Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.
Diffstat (limited to 'src/preprocessing/passes')
| -rw-r--r-- | src/preprocessing/passes/bv_ackermann.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/preprocessing/passes/bv_ackermann.cpp b/src/preprocessing/passes/bv_ackermann.cpp index 850136f9d..b5f152129 100644 --- a/src/preprocessing/passes/bv_ackermann.cpp +++ b/src/preprocessing/passes/bv_ackermann.cpp @@ -55,7 +55,12 @@ void storeFunction( if (set.find(term) == set.end()) { set.insert(term); - Node skolem = bv::utils::mkVar(bv::utils::getSize(term)); + TypeNode tn = term.getType(); + Node skolem = NodeManager::currentNM()->mkSkolem( + "BVSKOLEM$$", + tn, + "is a variable created by the ackermannization " + "preprocessing pass for theory BV"); fun_to_skolem.addSubstitution(term, skolem); } } @@ -156,7 +161,7 @@ PreprocessingPassResult BVAckermann::applyInternal( } /* replace applications of UF by skolems */ - // FIXME for model building, github issue #1118) + // FIXME for model building, github issue #1901 for (unsigned i = 0, size = assertionsToPreprocess->size(); i < size; ++i) { assertionsToPreprocess->replace( |