summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quantifiers_rewriter.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.h')
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 0edea5fae..d1f819726 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -94,6 +94,7 @@ public:
static Node preprocess( Node n, bool isInst = false );
static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
+ static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false );
};/* class QuantifiersRewriter */
}/* CVC4::theory::quantifiers namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback