Yices2: rename constant for function-application or array-select.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java

@@ -15,7 +15,7 @@
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_CONST;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_GE_ATOM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_SUM;
-import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARRAY_EVAL;
+import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARRAY_SELECT;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BIT_TERM;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BOOL_CONST;
 import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BV_ARRAY;
@@ -477,7 +477,7 @@ private <R> R visitFunctionApplication(
           functionKind = FunctionDeclarationKind.SELECT;
           functionArgs = getArgs(pF);
           functionName = "select";
-          functionDeclaration = -YICES_ARRAY_EVAL;
+          functionDeclaration = -YICES_ARRAY_SELECT;
         }
         break;
       case YICES_UPDATE_TERM:
@@ -843,7 +843,7 @@ public Integer callFunctionImpl(Integer pDeclaration, List<Integer> pArgs) {
           return yices_bvproduct(pArgs.size(), Ints.toArray(pArgs));
         case YICES_AND:
           return yices_and(pArgs.size(), Ints.toArray(pArgs));
-        case YICES_ARRAY_EVAL:
+        case YICES_ARRAY_SELECT:
           return yices_application(pArgs.get(0), 1, new int[] {pArgs.get(1)});
         case YICES_UPDATE_TERM:
           return yices_update(pArgs.get(0), 1, new int[] {pArgs.get(1)}, pArgs.get(2));

src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java

@@ -89,7 +89,7 @@ private Yices2NativeApi() {}
   // MAX_INT avoids collisions with existing constants
   public static final int YICES_AND = Integer.MAX_VALUE - 1;
   public static final int YICES_BV_MUL = Integer.MAX_VALUE - 2;
-  public static final int YICES_ARRAY_EVAL = Integer.MAX_VALUE - 3;
+  public static final int YICES_ARRAY_SELECT = Integer.MAX_VALUE - 3;
 
   /*
    * Yices model tags