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

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e691788fa..181632812 100644
--- 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);