Z3: use utility method instead of direct access.

The method potentially matches more cases, like multiple instance of TRUE or FALSE.
However, I have not yet seen two instances of TRUE or FALSE in Z3.

src/org/sosy_lab/java_smt/solvers/z3/Z3BooleanFormulaManager.java

@@ -8,7 +8,10 @@
 
 package org.sosy_lab.java_smt.solvers.z3;
 
+import static org.sosy_lab.java_smt.solvers.z3.Z3FormulaCreator.isOP;
+
 import com.microsoft.z3.Native;
+import com.microsoft.z3.enumerations.Z3_decl_kind;
 import java.util.Collection;
 import java.util.stream.Collector;
 import java.util.stream.Collectors;
@@ -153,12 +156,12 @@ protected Long implication(Long pBits1, Long pBits2) {
 
   @Override
   protected boolean isTrue(Long pParam) {
-    return Native.isEqAst(z3context, pParam, z3true);
+    return isOP(z3context, pParam, Z3_decl_kind.Z3_OP_TRUE);
   }
 
   @Override
   protected boolean isFalse(Long pParam) {
-    return Native.isEqAst(z3context, pParam, z3false);
+    return isOP(z3context, pParam, Z3_decl_kind.Z3_OP_FALSE);
   }
 
   @Override

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -772,8 +772,8 @@ public boolean isConstant(long value) {
     return Native.isNumeralAst(environment, value)
         || Native.isAlgebraicNumber(environment, value)
         || Native.isString(environment, value)
-        || isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE.toInt())
-        || isOP(environment, value, Z3_decl_kind.Z3_OP_FALSE.toInt());
+        || isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE)
+        || isOP(environment, value, Z3_decl_kind.Z3_OP_FALSE);
   }
 
   /**
@@ -798,7 +798,7 @@ public Object convertValue(Long value) {
     try {
       FormulaType<?> type = getFormulaType(value);
       if (type.isBooleanType()) {
-        return isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE.toInt());
+        return isOP(environment, value, Z3_decl_kind.Z3_OP_TRUE);
       } else if (type.isIntegerType()) {
         return new BigInteger(Native.getNumeralString(environment, value));
       } else if (type.isRationalType()) {
@@ -845,13 +845,13 @@ protected Long getBooleanVarDeclarationImpl(Long pLong) {
   }
 
   /** returns, if the function of the expression is the given operation. */
-  static boolean isOP(long z3context, long expr, int op) {
+  static boolean isOP(long z3context, long expr, Z3_decl_kind op) {
     if (!Native.isApp(z3context, expr)) {
       return false;
     }
 
     long decl = Native.getAppDecl(z3context, expr);
-    return Native.getDeclKind(z3context, decl) == op;
+    return Native.getDeclKind(z3context, decl) == op.toInt();
   }
 
   /**