Adds statistics for the number of Uservariables and Slack variables used by arithmetic.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e691788fa5b77095775cf65a70440d93c2490551..18163281243e58ce7b02f569eaab600e9e80a8bd 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -124,6 +124,7 @@ void TheoryArith::preRegisterTerm(TNode n) {
   }
 
   if(isTheoryLeaf(n) || isStrictlyVarList){
+    ++(d_statistics.d_statUserVariables);
     ArithVar varN = requestArithVar(n,false);
     setupInitialValue(varN);
   }
@@ -197,6 +198,9 @@ void TheoryArith::asVectors(Polynomial& p, std::vector<Rational>& coeffs, std::v
 
 void TheoryArith::setupSlack(TNode left){
 
+  
+
+  ++(d_statistics.d_statSlackVariables);
   TypeNode real_type = NodeManager::currentNM()->realType();
   Node slack = NodeManager::currentNM()->mkVar(real_type);
   left.setAttribute(Slack(), slack);