diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 5929e2db3f..561e88c43f 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -88,7 +88,9 @@ public Term makeVariable(Sort sort, String name) { Preconditions.checkArgument( sort.equals(exp.getSort()), "symbol name %s with sort %s already in use for different sort %s", - name, sort, exp.getSort()); + name, + sort, + exp.getSort()); return exp; } @@ -228,8 +230,7 @@ public T encapsulate(FormulaType pType, Term pTerm) { || (pType.equals(FormulaType.RationalType) && getFormulaType(pTerm).equals(FormulaType.IntegerType)) : String.format( - "Cannot encapsulate formula %s of Type %s as %s", - pTerm, getFormulaType(pTerm), pType); + "Cannot encapsulate formula %s of Type %s as %s", pTerm, getFormulaType(pTerm), pType); if (pType.isBooleanType()) { return (T) new CVC5BooleanFormula(pTerm); } else if (pType.isIntegerType()) { diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java index 809ec4001b..b663b57da2 100644 --- a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java @@ -163,8 +163,7 @@ public void testRegexAllCharUnicode() throws SolverException, InterruptedExcepti } else { // Z3 and other solvers support Unicode characters in the theory of strings. assertThatFormula( - smgr.in( - smgr.makeVariable("x"), smgr.union(smgr.range('a', 'Δ'), regexAllChar))) + smgr.in(smgr.makeVariable("x"), smgr.union(smgr.range('a', 'Δ'), regexAllChar))) .isSatisfiable(); // Combining characters are not matched as one character. // Non-ascii non-printable characters should use the codepoint representation @@ -191,7 +190,7 @@ public void testEmptyRegex() throws SolverException, InterruptedException { } @Test - public void testRegexUnion() throws SolverException, InterruptedException { + public void testRegexUnion() throws SolverException, InterruptedException { RegexFormula regex = smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")); assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isSatisfiable(); assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isSatisfiable(); @@ -199,22 +198,23 @@ public void testRegexUnion() throws SolverException, InterruptedException { } @Test - public void testRegexIntersection() throws SolverException, InterruptedException { + public void testRegexIntersection() throws SolverException, InterruptedException { RegexFormula regex = smgr.intersection(smgr.makeRegex("a"), smgr.makeRegex("b")); StringFormula variable = smgr.makeVariable("var"); assertThatFormula(smgr.in(variable, regex)).isUnsatisfiable(); - regex = smgr.intersection( - smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), - smgr.union(smgr.makeRegex("b"), smgr.makeRegex("c"))); + regex = + smgr.intersection( + smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), + smgr.union(smgr.makeRegex("b"), smgr.makeRegex("c"))); assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isUnsatisfiable(); assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isSatisfiable(); } @Test - public void testRegexDifference() throws SolverException, InterruptedException { - RegexFormula regex = smgr.difference( - smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), smgr.makeRegex("b")); + public void testRegexDifference() throws SolverException, InterruptedException { + RegexFormula regex = + smgr.difference(smgr.union(smgr.makeRegex("a"), smgr.makeRegex("b")), smgr.makeRegex("b")); assertThatFormula(smgr.in(smgr.makeString("a"), regex)).isSatisfiable(); assertThatFormula(smgr.in(smgr.makeString("b"), regex)).isUnsatisfiable(); }