Move first order model for full model check to own file (#5918)

[cvc5.git] / src / theory / rewriter.h

diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f38f3b174c28d17c4f732c1d1b31a1f6e5889946..572662483d19aa38280070961802ff31fa1fb181 100644 (file)
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -83,15 +83,12 @@ class Rewriter {
    * to setProofNodeManager prior to this call.
    *
    * @param node The node to rewrite.
-   * @param elimTheoryRewrite Whether we also want fine-grained proofs for
-   * THEORY_REWRITE steps.
    * @param isExtEq Whether node is an equality which we are applying
    * rewriteEqualityExt on.
    * @return The trust node of kind TrustNodeKind::REWRITE that contains the
    * rewritten form of node.
    */
   TrustNode rewriteWithProof(TNode node,
-                             bool elimTheoryRewrite = false,
                              bool isExtEq = false);
 
   /** Set proof node manager */
@@ -204,8 +201,6 @@ class Rewriter {
   /** Theory rewriters used by this rewriter instance */
   TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
 
-  unsigned long d_iterationCount = 0;
-
   /** Rewriter table for prewrites. Maps kinds to rewriter function. */
   std::function<RewriteResponse(RewriteEnvironment*, TNode)>
       d_preRewriters[kind::LAST_KIND];