Fix some documentation warnings (#8453)

diff --git a/.clang-format b/.clang-format
index fc35b4e00679a2119b352390541b834d6289ffd3..b240da02a1725ff0a8a254b1870dfa87f90baab3 100644 (file)
--- a/.clang-format
+++ b/.clang-format
@@ -24,8 +24,10 @@ AllowShortCaseLabelsOnASingleLine: true
 BinPackArguments: false
 BinPackParameters: false
 BreakBeforeBinaryOperators: NonAssignment
+BreakAfterJavaFieldAnnotations: false
 BraceWrapping:
   AfterCaseLabel: true
+  AfterObjCDeclaration: true
   AfterClass: true
   AfterControlStatement: true
   AfterEnum: true

diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 622af563b28575bce9a421bbae6382e743452c42..cf55b0589f1dcb41ffce21ba5bba278e36f18392 100644 (file)
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3932,7 +3932,6 @@ class CVC5_EXPORT Solver
    * @param terms the list of function bodies of the functions
    * @param global determines whether this definition is global (i.e. persists
    *               when popping the context)
-   * @return the function
    */
   void defineFunsRec(const std::vector<Term>& funs,
                      const std::vector<std::vector<Term>>& bound_vars,

diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java
index f4b73e1f4fc04ace1c32c1f19bd1b237f85dfdbb..6fdaaac377e1e88ef498b6aa85dd62fe15727afa 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Datatype.java
+++ b/src/api/java/io/github/cvc5/api/Datatype.java
@@ -116,7 +116,8 @@ public class Datatype extends AbstractPointer implements Iterable<DatatypeConstr
    * @return the parameters of this datatype, if it is parametric. An exception
    * is thrown if this datatype is not parametric.
    */
-  public Sort[] getParameters() {
+  public Sort[] getParameters()
+  {
     long[] sortPointers = getParameters(pointer);
     Sort[] sorts = Utils.getSorts(solver, sortPointers);
     return sorts;

diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
index da30b3d4a173d0b0633e20c4310ced3006b2a9e9..bd8b7d16342503a27f86a67a7a780fc8eb2e9158 100644 (file)
--- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
@@ -80,14 +80,13 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * @param retSort the desired return sort of the constructor
    * @return the constructor term
    */
-  public Term getInstantiatedConstructorTerm(Sort retSort) {
-    long termPointer =
-        getInstantiatedConstructorTerm(pointer, retSort.getPointer());
+  public Term getInstantiatedConstructorTerm(Sort retSort)
+  {
+    long termPointer = getInstantiatedConstructorTerm(pointer, retSort.getPointer());
     return new Term(solver, termPointer);
   }
 
-  private native long getInstantiatedConstructorTerm(
-      long pointer, long retSortPointer);
+  private native long getInstantiatedConstructorTerm(long pointer, long retSortPointer);
 
   /**
    * Get the tester operator of this datatype constructor.

diff --git a/src/api/java/io/github/cvc5/api/IPointer.java b/src/api/java/io/github/cvc5/api/IPointer.java
index 383ef51f6436286d86c5529a45ada169f48f2bba..233548db8ef17c5c3afd092ab79c57c773f7123f 100644 (file)
--- a/src/api/java/io/github/cvc5/api/IPointer.java
+++ b/src/api/java/io/github/cvc5/api/IPointer.java
@@ -15,7 +15,6 @@
 
 package io.github.cvc5.api;
 
-interface IPointer
-{
+interface IPointer {
   long getPointer();
 }

diff --git a/src/api/java/io/github/cvc5/api/OptionInfo.java b/src/api/java/io/github/cvc5/api/OptionInfo.java
index 1c47eeedb61503c6f72b74ae8f4f47d0550601b5..9ee43774cfcb005596e03024bc842b057340d4e8 100644 (file)
--- a/src/api/java/io/github/cvc5/api/OptionInfo.java
+++ b/src/api/java/io/github/cvc5/api/OptionInfo.java
@@ -206,4 +206,4 @@ public class OptionInfo extends AbstractPointer
   }
 
   private native double doubleValue(long pointer);
-};
+}

diff --git a/src/api/java/io/github/cvc5/api/Pair.java b/src/api/java/io/github/cvc5/api/Pair.java
index 6ebd8c2b27b64ec0ffb639d21b358a6456cba447..307273e5e8b5b78d7343b41df16a52c4a522c554 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Pair.java
+++ b/src/api/java/io/github/cvc5/api/Pair.java
@@ -32,8 +32,6 @@ public class Pair<K, V>
     if (pair == null || getClass() != pair.getClass())
       return false;
 
-    Pair<K, V> p = (Pair<K, V>) pair;
-
-    return first.equals(p.first) && second.equals(p.second);
+    return first.equals(((Pair<?, ?>) pair).first) && second.equals(((Pair<?, ?>) pair).second);
   }
 }

diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java
index 7af2013fd40b6091dd4330a5008b347e038d4f07..856986136af5a676a2e1c9e7c4cc10752f0c4c4b 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Result.java
+++ b/src/api/java/io/github/cvc5/api/Result.java
@@ -117,7 +117,8 @@ public class Result extends AbstractPointer
    * @return true if query was a checkSat() or checkSatAssuming() query and
    * cvc5 was not able to determine (un)satisfiability.
    */
-  public boolean isUnknown() {
+  public boolean isUnknown()
+  {
     return isUnknown(pointer);
   }
 

diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index 4b4c2ccc8b42f63d9739c040edbdc7bd69319204..b959cd0dac73ea1665d91a7e4f7bf39e6db67fc9 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -1790,7 +1790,8 @@ public class Solver implements IPointer, AutoCloseable
    *
    * @return the list of learned literals
    */
-  public Term[] getLearnedLiterals() {
+  public Term[] getLearnedLiterals()
+  {
     long[] retPointers = getLearnedLiterals(pointer);
     return Utils.getTerms(this, retPointers);
   }
@@ -2702,7 +2703,8 @@ public class Solver implements IPointer, AutoCloseable
    *         getSynthSolutions, "no solution" if it was determined there is no
    *         solution, or "unknown" otherwise.
    */
-  public SynthResult checkSynth() {
+  public SynthResult checkSynth()
+  {
     long resultPointer = checkSynth(pointer);
     return new SynthResult(this, resultPointer);
   }
@@ -2723,7 +2725,8 @@ public class Solver implements IPointer, AutoCloseable
    *         getSynthSolutions, "no solution" if it was determined there is no
    *         solution, or "unknown" otherwise.
    */
-  public SynthResult checkSynthNext() {
+  public SynthResult checkSynthNext()
+  {
     long resultPointer = checkSynthNext(pointer);
     return new SynthResult(this, resultPointer);
   }

diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index 0cd275070f5589864ad943c283797c235fe47bfc..a8199330252c44e7a847719ca441197e6cf38f63 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -368,7 +368,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
    *
    * An instantiated sort is a sort that has been constructed from
    * instantiating a sort with sort arguments
-   * (see Sort.instantiate()).
+   * (see {@link Sort#instantiate(Sort[])}).
    *
    * @return true if this is an instantiated sort
    */
@@ -428,7 +428,7 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   /**
    * Get the sorts used to instantiate the sort parameters of a parametric
    * sort (parametric datatype or uninterpreted sort constructor sort,
-   * see Sort.instantiate()).
+   * see {@link Sort#instantiate(Sort[])}).
    *
    * @return the sorts used to instantiate the sort parameters of a
    *         parametric sort

diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java
index df7a82c5866ab2e22cbd347548b8ae6d8e54f152..cf8a2c704a0c020b46389ddfa0cff655d1fe07c2 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Statistics.java
+++ b/src/api/java/io/github/cvc5/api/Statistics.java
@@ -15,10 +15,10 @@
 
 package io.github.cvc5.api;
 
+import java.util.AbstractMap;
 import java.util.Iterator;
-import java.util.NoSuchElementException;
 import java.util.Map;
-import java.util.AbstractMap;
+import java.util.NoSuchElementException;
 
 public class Statistics extends AbstractPointer implements Iterable<Map.Entry<String, Stat>>
 {
@@ -102,18 +102,13 @@ public class Statistics extends AbstractPointer implements Iterable<Map.Entry<St
         Pair<String, Long> pair = Statistics.this.getNext(pointer, iteratorPointer);
         Stat stat = new Stat(solver, pair.second);
         this.iteratorPointer = Statistics.this.increment(pointer, iteratorPointer);
-        return new AbstractMap.SimpleImmutableEntry(pair.first, stat);
+        return new AbstractMap.SimpleImmutableEntry<>(pair.first, stat);
       }
       catch (CVC5ApiException e)
       {
         throw new NoSuchElementException(e.getMessage());
       }
     }
-
-    @Override public void finalize()
-    {
-      deleteIteratorPointer(iteratorPointer);
-    }
   }
 
   public ConstIterator iterator(boolean internal, boolean defaulted)
@@ -124,4 +119,4 @@ public class Statistics extends AbstractPointer implements Iterable<Map.Entry<St
   {
     return new ConstIterator();
   }
-};
+}

diff --git a/src/api/java/io/github/cvc5/api/SynthResult.java b/src/api/java/io/github/cvc5/api/SynthResult.java
index fac196abfd7db51d845d4964926321a85bb7ddd2..d0b21b604ae47fb708b7c287970c3a6fd8a8cdd8 100644 (file)
--- a/src/api/java/io/github/cvc5/api/SynthResult.java
+++ b/src/api/java/io/github/cvc5/api/SynthResult.java
@@ -15,9 +15,6 @@
 
 package io.github.cvc5.api;
 
-import java.util.HashMap;
-import java.util.Map;
-
 public class SynthResult extends AbstractPointer
 {
   // region construction and destruction

diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java
index 02fb42cf4f412596552a2d49b612ba35a097f531..c8a1b9ddf95809fbd79af75e291333744b35ba91 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Term.java
+++ b/src/api/java/io/github/cvc5/api/Term.java
@@ -630,7 +630,7 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
   public Triplet<Long, Long, Term> getFloatingPointValue()
   {
     Triplet<Long, Long, Long> triplet = getFloatingPointValue(pointer);
-    return new Triplet(triplet.first, triplet.second, new Term(solver, triplet.third));
+    return new Triplet<>(triplet.first, triplet.second, new Term(solver, triplet.third));
   }
 
   private native Triplet<Long, Long, Long> getFloatingPointValue(long pointer);
@@ -692,7 +692,7 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
 
   private native boolean isCardinalityConstraint(long pointer);
 
- /**
+  /**
    * Asserts isCardinalityConstraint().
    * @return the sort the cardinality constraint is for and its upper bound.
    */

diff --git a/src/api/java/io/github/cvc5/api/Triplet.java b/src/api/java/io/github/cvc5/api/Triplet.java
index b9cd36d2ff6654bd6dc6b651775dca43621544b7..1b98ac4169c67f434c0e535b32eb72756829e6c5 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Triplet.java
+++ b/src/api/java/io/github/cvc5/api/Triplet.java
@@ -34,8 +34,8 @@ public class Triplet<A, B, C>
     if (object == null || getClass() != object.getClass())
       return false;
 
-    Triplet<A, B, C> triplet = (Triplet<A, B, C>) object;
-    return this.first.equals(triplet.first) && this.second.equals(triplet.second)
-        && this.third.equals(triplet.third);
+    return this.first.equals(((Triplet<?, ?, ?>) object).first)
+        && this.second.equals(((Triplet<?, ?, ?>) object).second)
+        && this.third.equals(((Triplet<?, ?, ?>) object).third);
   }
 }

diff --git a/src/api/java/io/github/cvc5/api/Utils.java b/src/api/java/io/github/cvc5/api/Utils.java
index 6254d43ba30056efe931ee8cc887dce210dd7d89..5c814a7f5f98c0812afd5680d931ab121bc9fe3d 100644 (file)
--- a/src/api/java/io/github/cvc5/api/Utils.java
+++ b/src/api/java/io/github/cvc5/api/Utils.java
@@ -15,7 +15,6 @@
 
 package io.github.cvc5.api;
 
-import java.io.IOException;
 import java.math.BigInteger;
 import java.util.ArrayList;
 import java.util.List;
@@ -131,6 +130,7 @@ public class Utils
     }
   }
 
+  @SuppressWarnings("unchecked")
   public static <K> Pair<K, Long>[] getPairs(Pair<K, ? extends AbstractPointer>[] abstractPointers)
   {
     Pair<K, Long>[] pointers = new Pair[abstractPointers.length];

diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index 8e05cb16475f143df4e74126b51fd5f9cedba17f..aeea03d56afe32c7d52b87792ae1d3550d40b303 100644 (file)
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -541,12 +541,10 @@ class DatatypeTest
 
     AtomicReference<Term> atomicTerm = new AtomicReference<>();
     // get the specialized constructor term for list[Int]
-    assertDoesNotThrow(
-        () -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt)));
+    assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt)));
     Term testConsTerm = atomicTerm.get();
     assertNotEquals(testConsTerm, nilc.getConstructorTerm());
     // error to get the specialized constructor term for Int
-    assertThrows(CVC5ApiException.class,
-        () -> nilc.getInstantiatedConstructorTerm(isort));
+    assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedConstructorTerm(isort));
   }
 }

diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index 9f93c54b05b6fb92b63e5ff2f78d2a68368597b1..4cca6e71181d4f1051fa6ab1af14746ab6444388 100644 (file)
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -173,8 +173,7 @@ class OpTest
     Op tupleProject = d_solver.mkOp(TUPLE_PROJECT, indices);
     for (int i = 0, size = tupleProject.getNumIndices(); i < size; i++)
     {
-      assertEquals(
-          indices[i], tupleProject.get(i).getIntegerValue().intValue());
+      assertEquals(indices[i], tupleProject.get(i).getIntegerValue().intValue());
     }
   }
 

diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java
index f21d5e8f03a82f22bfc043c6f388e3efb1e668fe..ffe1ee412c0ee7cf1033772cc14a7050b42fc91c 100644 (file)
--- a/test/unit/api/java/ResultTest.java
+++ b/test/unit/api/java/ResultTest.java
@@ -83,8 +83,8 @@ class ResultTest
     assertFalse(res.isUnknown());
   }
 
-  @Test
-  void isUnknown() throws CVC5ApiException {
+  @Test void isUnknown() throws CVC5ApiException
+  {
     d_solver.setLogic("QF_NIA");
     d_solver.setOption("incremental", "false");
     d_solver.setOption("solve-int-as-bv", "32");

diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index e678d3d50bab91f737b55386d4f77ca09c952b57..58fe0d9e707b2d9bfe396fcc11e37d49e37d7a5a 100644 (file)
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -1350,7 +1350,7 @@ class SolverTest
     Sort bsort = d_solver.getBooleanSort();
     Term truen = d_solver.mkBoolean(true);
     Term start = d_solver.mkVar(bsort);
-    Term output2  = d_solver.getNullTerm();
+    Term output2 = d_solver.getNullTerm();
     Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
     Term conj2 = d_solver.mkTerm(GT, x, zero);
     assertDoesNotThrow(() -> g.addRule(start, truen));
@@ -1372,7 +1372,7 @@ class SolverTest
     d_solver.assertFormula(d_solver.mkTerm(GT, x, zero));
     // Conjecture for abduction: y > 0
     Term conj = d_solver.mkTerm(GT, y, zero);
-    Term output  = d_solver.getNullTerm();
+    Term output = d_solver.getNullTerm();
     // Fails due to option not set
     assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj));
   }
@@ -1399,7 +1399,6 @@ class SolverTest
     assertNotEquals(output, output2);
   }
 
-
   @Test void getInterpolant() throws CVC5ApiException
   {
     d_solver.setLogic("QF_LIA");
@@ -1519,14 +1518,14 @@ class SolverTest
       assertions.add(() -> assertEquals("print-success", info.getName()));
       assertions.add(
           () -> assertEquals(Arrays.asList(new String[] {}), Arrays.asList(info.getAliases())));
-      assertions.add(
-          () -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class));
-      OptionInfo.ValueInfo<Boolean> valInfo =
-          (OptionInfo.ValueInfo<Boolean>) info.getBaseInfo();
+      assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class));
+      OptionInfo.ValueInfo<Boolean> valInfo = (OptionInfo.ValueInfo<Boolean>) info.getBaseInfo();
       assertions.add(() -> assertEquals(false, valInfo.getDefaultValue().booleanValue()));
       assertions.add(() -> assertEquals(false, valInfo.getCurrentValue().booleanValue()));
       assertions.add(() -> assertEquals(info.booleanValue(), false));
-      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ print-success | bool | false | default false }"));
+      assertions.add(()
+                         -> assertEquals(info.toString(),
+                             "OptionInfo{ print-success | bool | false | default false }"));
     }
     {
       // int64 type with default
@@ -1543,14 +1542,14 @@ class SolverTest
       assertions.add(
           () -> assertTrue(numInfo.getMinimum() == null && numInfo.getMaximum() == null));
       assertions.add(() -> assertEquals(info.intValue().intValue(), 0));
-      assertions.add(() -> assertEquals(info.toString(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }"));
+      assertions.add(
+          () -> assertEquals(info.toString(), "OptionInfo{ verbosity | int64_t | 0 | default 0 }"));
     }
     assertAll(assertions);
     {
       OptionInfo info = d_solver.getOptionInfo("rlimit");
       assertEquals(info.getName(), "rlimit");
-      assertEquals(
-          Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
+      assertEquals(Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
       assertTrue(info.getBaseInfo().getClass() == OptionInfo.NumberInfo.class);
       OptionInfo.NumberInfo<BigInteger> ni = (OptionInfo.NumberInfo<BigInteger>) info.getBaseInfo();
       assertEquals(ni.getCurrentValue().intValue(), 0);
@@ -1572,13 +1571,13 @@ class SolverTest
       assertEquals(ni.getMinimum(), 0.0);
       assertEquals(ni.getMaximum(), 1.0);
       assertEquals(info.doubleValue(), 0.0);
-      assertEquals(info.toString(), "OptionInfo{ random-freq, random-frequency | double | 0 | default 0 | 0 <= x <= 1 }");
+      assertEquals(info.toString(),
+          "OptionInfo{ random-freq, random-frequency | double | 0 | default 0 | 0 <= x <= 1 }");
     }
     {
       OptionInfo info = d_solver.getOptionInfo("force-logic");
       assertEquals(info.getName(), "force-logic");
-      assertEquals(
-          Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
+      assertEquals(Arrays.asList(info.getAliases()), Arrays.asList(new String[] {}));
       assertTrue(info.getBaseInfo().getClass() == OptionInfo.ValueInfo.class);
       OptionInfo.ValueInfo<String> ni = (OptionInfo.ValueInfo<String>) info.getBaseInfo();
       assertEquals(ni.getCurrentValue(), "");
@@ -1591,8 +1590,9 @@ class SolverTest
       OptionInfo info = d_solver.getOptionInfo("simplification");
       assertions.clear();
       assertions.add(() -> assertEquals("simplification", info.getName()));
-      assertions.add(
-          () -> assertEquals(Arrays.asList(new String[] {"simplification-mode"}), Arrays.asList(info.getAliases())));
+      assertions.add(()
+                         -> assertEquals(Arrays.asList(new String[] {"simplification-mode"}),
+                             Arrays.asList(info.getAliases())));
       assertions.add(() -> assertTrue(info.getBaseInfo().getClass() == OptionInfo.ModeInfo.class));
       OptionInfo.ModeInfo modeInfo = (OptionInfo.ModeInfo) info.getBaseInfo();
       assertions.add(() -> assertEquals("batch", modeInfo.getDefaultValue()));
@@ -1600,7 +1600,8 @@ class SolverTest
       assertions.add(() -> assertEquals(2, modeInfo.getModes().length));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("batch")));
       assertions.add(() -> assertTrue(Arrays.asList(modeInfo.getModes()).contains("none")));
-      assertEquals(info.toString(), "OptionInfo{ simplification, simplification-mode | mode | batch | default batch | modes: batch, none }");
+      assertEquals(info.toString(),
+          "OptionInfo{ simplification, simplification-mode | mode | batch | default batch | modes: batch, none }");
     }
     assertAll(assertions);
   }
@@ -1630,7 +1631,10 @@ class SolverTest
       assertTrue(s.isInt());
       assertTrue(s.getInt() >= 0);
     }
-    for (Map.Entry<String, Stat> s : stats) {}
+    for (Map.Entry<String, Stat> s : stats)
+    {
+      assertFalse(s.getKey().isEmpty());
+    }
     for (Statistics.ConstIterator it = stats.iterator(true, true); it.hasNext();)
     {
       Map.Entry<String, Stat> elem = it.next();
@@ -1774,8 +1778,8 @@ class SolverTest
     }
   }
 
-  @Test
-  void getLearnedLiterals() {
+  @Test void getLearnedLiterals()
+  {
     d_solver.setOption("produce-learned-literals", "true");
     // cannot ask before a check sat
     assertThrows(CVC5ApiException.class, () -> d_solver.getLearnedLiterals());
@@ -1783,8 +1787,8 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.getLearnedLiterals());
   }
 
-  @Test
-  void getLearnedLiterals2() {
+  @Test void getLearnedLiterals2()
+  {
     d_solver.setOption("produce-learned-literals", "true");
     Sort intSort = d_solver.getIntegerSort();
     Term x = d_solver.mkConst(intSort, "x");
@@ -1792,8 +1796,7 @@ class SolverTest
     Term zero = d_solver.mkInteger(0);
     Term ten = d_solver.mkInteger(10);
     Term f0 = d_solver.mkTerm(GEQ, x, ten);
-    Term f1 = d_solver.mkTerm(
-        OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
+    Term f1 = d_solver.mkTerm(OR, d_solver.mkTerm(GEQ, zero, x), d_solver.mkTerm(GEQ, y, zero));
     d_solver.assertFormula(f0);
     d_solver.assertFormula(f1);
     d_solver.checkSat();
@@ -2469,7 +2472,8 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.declareSygusVar(funSort, ""));
 
     assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort()));
-    assertThrows(CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort(), "a"));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.declareSygusVar(d_solver.getNullSort(), "a"));
 
     Solver slv = new Solver();
     slv.setOption("sygus", "true");