Explicitly blacklist all predefined bv functions as variable/uf names.

Not allowing any variable names starting with "bv" lead to too many issues as the prefix is used frequently throughout the tests.

Author: daniel-raffler

src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java

@@ -112,8 +112,34 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
           // Bitvectors
           "concat",
           "extract",
-          // + any symbol starting with "bv"
+          "zero_extend",
+          "sign_extend",
+          "rotate_left",
+          "rotate_right",
+          "bv2int",
+          "int2bv",
+          "bvadd",
+          "bvsub",
           "bvneg",
+          "bvmul",
+          "bvurem",
+          "bvsrem",
+          "bvsmod",
+          "bvshl",
+          "bvlshr",
+          "bvashr",
+          "bvor",
+          "bvand",
+          "bvnot",
+          "bvxor",
+          "bvule",
+          "bvult",
+          "bvuge",
+          "bvugt",
+          "bvsle",
+          "bvslt",
+          "bvsge",
+          "bvsgt",
 
           // Core
           "true",
@@ -181,8 +207,7 @@ public abstract class AbstractFormulaManager<TFormulaInfo, TType, TEnv, TFuncDec
    * solvers.
    */
   public static boolean isReserved(String pVar) {
-    return pVar.startsWith("bv")
-        || pVar.startsWith("fp.*")
+    return pVar.startsWith("fp.")
         || pVar.startsWith("str.")
         || pVar.startsWith("re.")
         || RESERVED.contains(pVar);