diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java index d475a00284..ef1ef96205 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessAbstractProver.java @@ -121,7 +121,7 @@ protected void popImpl() { // we have to recreate symbols on lower levels, because JavaSMT assumes "global" symbols. Level level = trackingStack.pop(); api.addBooleanVariables(asScala(level.booleanSymbols)); - api.addConstants(asScala(level.intSymbols)); + api.addConstants(asScala(level.theorySymbols)); level.functionSymbols.forEach(api::addFunction); if (!trackingStack.isEmpty()) { trackingStack.peek().mergeWithHigher(level); @@ -213,12 +213,12 @@ void addSymbol(IFormula f) { } } - /** add external definition: integer variable. */ + /** add external definition: theory variable (integer, rational, string, etc). */ void addSymbol(ITerm f) { Preconditions.checkState(!closed); api.addConstant(f); if (!trackingStack.isEmpty()) { - trackingStack.peek().intSymbols.add(f); + trackingStack.peek().theorySymbols.add(f); } } @@ -233,7 +233,7 @@ void addSymbol(IFunction f) { static class Level { final List booleanSymbols = new ArrayList<>(); - final List intSymbols = new ArrayList<>(); + final List theorySymbols = new ArrayList<>(); final List functionSymbols = new ArrayList<>(); Level() {} @@ -241,13 +241,13 @@ static class Level { /** add higher level to current level, we keep the order of creating symbols. */ void mergeWithHigher(Level other) { this.booleanSymbols.addAll(other.booleanSymbols); - this.intSymbols.addAll(other.intSymbols); + this.theorySymbols.addAll(other.theorySymbols); this.functionSymbols.addAll(other.functionSymbols); } @Override public String toString() { - return String.format("{%s, %s, %s}", booleanSymbols, intSymbols, functionSymbols); + return String.format("{%s, %s, %s}", booleanSymbols, theorySymbols, functionSymbols); } } }