From 296d8e40c092c49faa844befe1ccb7d26ede6576 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Tue, 10 Sep 2024 19:42:15 +0200
Subject: [PATCH] Princess: Renamed list of (non-boolean) variables in
 PrincessAbstractProver from intSymbols` to `theorySymbols` as it may not only
 contain integer variables.

---
 .../solvers/princess/PrincessAbstractProver.java     | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

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<IFormula> booleanSymbols = new ArrayList<>();
-    final List<ITerm> intSymbols = new ArrayList<>();
+    final List<ITerm> theorySymbols = new ArrayList<>();
     final List<IFunction> 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);
     }
   }
 }