diff --git a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala index 3ffb5c532d19313b17747ff546609e9402739c7e..aee689be4bd1a1f89760272220e71132cbba8549 100644 --- a/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala +++ b/src/main/scala/leon/invariant/structure/LinearConstraintUtil.scala @@ -376,7 +376,7 @@ object LinearConstraintUtil { } case _ => Seq() // drop constraints with `oneSidedVars` } ++ currEqs).distinct // note: this is very important!! - Stats.updateCounterStats(currEqs.size, "UneliminatedEqualities", "disjuncts") + Stats.updateCumStats(currEqs.size, "UneliminatedEqualities") resctrs } diff --git a/src/test/scala/leon/unit/orb/OrbUnitTestSuite.scala b/src/test/scala/leon/unit/orb/OrbUnitTestSuite.scala index 32229100b782b154a360843d2a4d3dd6ffa4f210..ac6a65f71602e8c73769bd3e9c81c350eabfc243 100644 --- a/src/test/scala/leon/unit/orb/OrbUnitTestSuite.scala +++ b/src/test/scala/leon/unit/orb/OrbUnitTestSuite.scala @@ -41,20 +41,20 @@ class OrbUnitTestSuite extends LeonTestSuite { test("TestElimination") {ctx => val exprs = Seq(Equals(a, b), Equals(c, Plus(a, b)), GreaterEquals(Plus(c, d), zero)) - println("Exprs: "+exprs) - val elimVars = Set(a, b, c).map(_.id) + //println("Exprs: "+exprs) + val retainVars = Set(d).map(_.id) val ctrs = exprs map ConstraintUtil.createConstriant - val nctrs = apply1PRuleOnDisjunct(ctrs.collect{ case c: LinearConstraint => c }, elimVars, None) + val nctrs = apply1PRuleOnDisjunct(ctrs.collect{ case c: LinearConstraint => c }, retainVars, None) //println("Constraints after elimination: "+nctrs) assert(nctrs.size == 1) } test("TestElimination2") {ctx => val exprs = Seq(Equals(zero, Plus(a, b)), Equals(a, zero), GreaterEquals(Plus(b, c), zero)) - println("Exprs: "+exprs) - val elimVars = Set(a, b).map(_.id) + //println("Exprs: "+exprs) + val retainVars = Set(c).map(_.id) val ctrs = exprs map ConstraintUtil.createConstriant - val nctrs = apply1PRuleOnDisjunct(ctrs.collect{ case c: LinearConstraint => c }, elimVars, None) + val nctrs = apply1PRuleOnDisjunct(ctrs.collect{ case c: LinearConstraint => c }, retainVars, None) //println("Constraints after elimination: "+nctrs) assert(nctrs.size == 1) }