diff options
Diffstat (limited to 'src/util/ite_removal.h')
| -rw-r--r-- | src/util/ite_removal.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index 83c55dab7..d71f9b13d 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -50,8 +50,11 @@ public: * contains a map from introduced skolem variables to the index in * assertions containing the new Boolean ite created in conjunction * with that skolem variable. + * + * With reportDeps true, report reasoning dependences to the proof + * manager (for unsat cores). */ - void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap); + void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); /** * Removes the ITE from the node by introducing skolem |