Fixed formating

sosy-lab · Jan 3, 2024 · ff0b515 · ff0b515
1 parent 32d3dcd
commit ff0b515
Show file tree

Hide file tree

Showing 3 changed files with 53 additions and 50 deletions.
diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5NativeApiTest.java
@@ -537,7 +537,6 @@ public void enumTypeTest() throws SolverException, InterruptedException {
 
   private final ExecutorService executor = Executors.newSingleThreadExecutor();
 
-
   @SuppressWarnings("unused")
   private long createSharedEnv(long sibling) {
     long cfg = msat_create_config();
@@ -569,13 +568,15 @@ public void bug339Test() throws ExecutionException, InterruptedException {
     long prover = createSharedEnv(this.env);
     msat_assert_formula(prover, formula);
 
-    Future<?> task1 = executor.submit(() -> {
-      try {
-        assertThat(msat_check_sat(prover)).isFalse();
-      } catch (InterruptedException | SolverException pE) {
-        throw new RuntimeException(pE);
-      }
-    });
+    Future<?> task1 =
+        executor.submit(
+            () -> {
+              try {
+                assertThat(msat_check_sat(prover)).isFalse();
+              } catch (InterruptedException | SolverException pE) {
+                throw new RuntimeException(pE);
+              }
+            });
 
     assert task1.get() == null;
   }

diff --git a/src/org/sosy_lab/java_smt/test/Bug339Test.java b/src/org/sosy_lab/java_smt/test/Bug339Test.java
@@ -71,6 +71,6 @@ public void fixedTest() throws InterruptedException, ExecutionException {
               }
             });
 
-      assert task1.get() == null;
+    assert task1.get() == null;
   }
 }
diff --git a/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java b/src/org/sosy_lab/java_smt/test/SolverThreadLocalTest.java
@@ -218,36 +218,37 @@ public <T> void nonlocalInterpolationTest() throws InterruptedException, Executi
         (InterpolatingProverEnvironment<T>) context.newProverEnvironmentWithInterpolation()) {
       T id1 = prover.push(f1);
 
-      Future<?> task1 = executor.submit(
-          () -> {
-            try {
-              // FIXME: Exception for CVC5
-              // java.lang.IllegalStateException:
-              // You tried to use push() on an CVC5 assertion stack illegally.
-              //   at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl
-              //       (CVC5AbstractProver.java:89)
-              //   at org.sosy_lab.java_smt.basicimpl.AbstractProver.push
-              //       (AbstractProver.java:88)
-              //   at ..
-              prover.push(f2);
-
-              // FIXME: Exception for MathSAT (bug #339)
-              // java.lang.StackOverflowError
-              //   at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve
-              //       (Native Method)
-              //   at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat
-              //       (Mathsat5NativeApi.java:156)
-              //   at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat
-              //       (Mathsat5AbstractProver.java:106)
-              //   at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable
-              //       (ProverEnvironmentSubject.java:67)
-              //   at ..
-              assertThat(prover).isUnsatisfiable();
-
-            } catch (SolverException | InterruptedException pE) {
-              throw new RuntimeException(pE);
-            }
-          });
+      Future<?> task1 =
+          executor.submit(
+              () -> {
+                try {
+                  // FIXME: Exception for CVC5
+                  // java.lang.IllegalStateException:
+                  // You tried to use push() on an CVC5 assertion stack illegally.
+                  //   at org.sosy_lab.java_smt.solvers.cvc5.CVC5AbstractProver.pushImpl
+                  //       (CVC5AbstractProver.java:89)
+                  //   at org.sosy_lab.java_smt.basicimpl.AbstractProver.push
+                  //       (AbstractProver.java:88)
+                  //   at ..
+                  prover.push(f2);
+
+                  // FIXME: Exception for MathSAT (bug #339)
+                  // java.lang.StackOverflowError
+                  //   at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_solve
+                  //       (Native Method)
+                  //   at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_check_sat
+                  //       (Mathsat5NativeApi.java:156)
+                  //   at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5AbstractProver.isUnsat
+                  //       (Mathsat5AbstractProver.java:106)
+                  //   at org.sosy_lab.java_smt.test.ProverEnvironmentSubject.isUnsatisfiable
+                  //       (ProverEnvironmentSubject.java:67)
+                  //   at ..
+                  assertThat(prover).isUnsatisfiable();
+
+                } catch (SolverException | InterruptedException pE) {
+                  throw new RuntimeException(pE);
+                }
+              });
 
       assert task1.get() == null;
 
@@ -271,19 +272,20 @@ public <T> void nonlocalInterpolationTest() throws InterruptedException, Executi
       executor.awaitTermination(100, TimeUnit.MILLISECONDS);
       prover.pop();
 
-      Future<?> task3 = executor.submit(
-          () -> {
-            try {
-              prover.pop();
+      Future<?> task3 =
+          executor.submit(
+              () -> {
+                try {
+                  prover.pop();
 
-              prover.push(itp.get());
-              prover.push(f2);
+                  prover.push(itp.get());
+                  prover.push(f2);
 
-              assertThat(prover).isUnsatisfiable();
-            } catch (SolverException | InterruptedException | ExecutionException pE) {
-              throw new RuntimeException(pE);
-            }
-          });
+                  assertThat(prover).isUnsatisfiable();
+                } catch (SolverException | InterruptedException | ExecutionException pE) {
+                  throw new RuntimeException(pE);
+                }
+              });
 
       assert task3.get() == null;
     }