diff --git a/src/api/java/Context.java b/src/api/java/Context.java index b6cf690c4..a5e846cce 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -566,6 +566,7 @@ public class Context implements AutoCloseable { /** * Create a quantifier pattern. **/ + @SafeVarargs public Pattern mkPattern(Expr... terms) { if (terms.length == 0) @@ -687,6 +688,7 @@ public class Context implements AutoCloseable { /** * Create a new function application. **/ + @SafeVarargs public Expr mkApp(FuncDecl f, Expr... args) { checkContextMatch(f); @@ -732,6 +734,7 @@ public class Context implements AutoCloseable { /** * Creates a {@code distinct} term. **/ + @SafeVarargs public BoolExpr mkDistinct(Expr... args) { checkContextMatch(args); @@ -800,6 +803,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t[0] and t[1] and ...}. **/ + @SafeVarargs public BoolExpr mkAnd(Expr... t) { checkContextMatch(t); @@ -810,6 +814,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t[0] or t[1] or ...}. **/ + @SafeVarargs public BoolExpr mkOr(Expr... t) { checkContextMatch(t); @@ -820,6 +825,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t[0] + t[1] + ...}. **/ + @SafeVarargs public ArithExpr mkAdd(Expr... t) { checkContextMatch(t); @@ -830,6 +836,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t[0] * t[1] * ...}. **/ + @SafeVarargs public ArithExpr mkMul(Expr... t) { checkContextMatch(t); @@ -840,6 +847,7 @@ public class Context implements AutoCloseable { /** * Create an expression representing {@code t[0] - t[1] - ...}. **/ + @SafeVarargs public ArithExpr mkSub(Expr... t) { checkContextMatch(t); @@ -1814,6 +1822,7 @@ public class Context implements AutoCloseable { * @see #mkStore **/ + @SafeVarargs public ArrayExpr mkMap(FuncDecl f, Expr>... args) { checkContextMatch(f); @@ -1903,6 +1912,7 @@ public class Context implements AutoCloseable { /** * Take the union of a list of sets. **/ + @SafeVarargs public ArrayExpr mkSetUnion(Expr>... args) { checkContextMatch(args); @@ -1914,6 +1924,7 @@ public class Context implements AutoCloseable { /** * Take the intersection of a list of sets. **/ + @SafeVarargs public ArrayExpr mkSetIntersection(Expr>... args) { checkContextMatch(args); @@ -2018,6 +2029,7 @@ public class Context implements AutoCloseable { /** * Concatenate sequences. */ + @SafeVarargs public SeqExpr mkConcat(Expr>... t) { checkContextMatch(t); @@ -2182,6 +2194,7 @@ public class Context implements AutoCloseable { /** * Create the concatenation of regular languages. */ + @SafeVarargs public ReExpr mkConcat(ReExpr... t) { checkContextMatch(t); @@ -2191,6 +2204,7 @@ public class Context implements AutoCloseable { /** * Create the union of regular languages. */ + @SafeVarargs public ReExpr mkUnion(Expr>... t) { checkContextMatch(t); @@ -2200,6 +2214,7 @@ public class Context implements AutoCloseable { /** * Create the intersection of regular languages. */ + @SafeVarargs public ReExpr mkIntersect(Expr>... t) { checkContextMatch(t);