diff options
Diffstat (limited to 'src/theory/bv/abstraction.cpp')
| -rw-r--r-- | src/theory/bv/abstraction.cpp | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/theory/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp index d3aeb5c37..f2f12a548 100644 --- a/src/theory/bv/abstraction.cpp +++ b/src/theory/bv/abstraction.cpp @@ -95,10 +95,10 @@ bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, // we did not change anything return false; } - NodeNodeMap seen; + NodeNodeMap seen_rev; for (unsigned i = 0; i < new_assertions.size(); ++i) { - new_assertions[i] = reverseAbstraction(new_assertions[i], seen); + new_assertions[i] = reverseAbstraction(new_assertions[i], seen_rev); } // we undo the abstraction functions so the logic is QF_BV still return true; @@ -235,13 +235,15 @@ void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) // enumerate arguments assignments std::vector<Node> or_assignments; - for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); ++it) + for (const ArgsVec& av : args) + // for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); + // ++it) { NodeBuilder<> arg_assignment(kind::AND); - ArgsVec& args = *it; - for (unsigned k = 0; k < args.size(); ++k) + // ArgsVec& args = *it; + for (unsigned k = 0; k < av.size(); ++k) { - Node eq = nm->mkNode(kind::EQUAL, args[k], skolem_args[k]); + Node eq = nm->mkNode(kind::EQUAL, av[k], skolem_args[k]); arg_assignment << eq; } or_assignments.push_back(arg_assignment); |