fix warnings from SpotBugs.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorAbstractProver.java

@@ -33,7 +33,8 @@ abstract class BoolectorAbstractProver<T> extends AbstractProverWithAllSat<T> {
   private final long btor;
   private final BoolectorFormulaManager manager;
   private final BoolectorFormulaCreator creator;
-  protected boolean wasLastSatCheckSat = false; // and stack is not changed
+  protected final AtomicBoolean wasLastSatCheckSat =
+      new AtomicBoolean(false); // and stack is not changed
   private final TerminationCallback terminationCallback;
   private final long terminationCallbackHelper;
 
@@ -83,10 +84,10 @@ public void close() {
   @Override
   public boolean isUnsat() throws SolverException, InterruptedException {
     Preconditions.checkState(!closed);
-    wasLastSatCheckSat = false;
+    wasLastSatCheckSat.set(false);
     final int result = BtorJNI.boolector_sat(btor);
     if (result == BtorJNI.BTOR_RESULT_SAT_get()) {
-      wasLastSatCheckSat = true;
+      wasLastSatCheckSat.set(true);
       return false;
     } else if (result == BtorJNI.BTOR_RESULT_UNSAT_get()) {
       return true;
@@ -127,7 +128,7 @@ public boolean isUnsatWithAssumptions(Collection<BooleanFormula> pAssumptions)
   @Override
   public Model getModel() throws SolverException {
     Preconditions.checkState(!closed);
-    Preconditions.checkState(wasLastSatCheckSat, NO_MODEL_HELP);
+    Preconditions.checkState(wasLastSatCheckSat.get(), NO_MODEL_HELP);
     checkGenerateModels();
     return new CachingModel(getEvaluatorWithoutChecks());
   }

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorSolverContext.java

@@ -63,7 +63,7 @@ private static class BoolectorSettings {
   private final BoolectorFormulaManager manager;
   private final BoolectorFormulaCreator creator;
   private final ShutdownNotifier shutdownNotifier;
-  private boolean closed = false;
+  private final AtomicBoolean closed = new AtomicBoolean(false);
   private final AtomicBoolean isAnyStackAlive = new AtomicBoolean(false);
 
   BoolectorSolverContext(
@@ -188,16 +188,15 @@ public ImmutableMap<String, String> getStatistics() {
 
   @Override
   public void close() {
-    if (!closed) {
-      closed = true;
+    if (!closed.getAndSet(true)) {
       BtorJNI.boolector_delete(creator.getEnv());
     }
   }
 
   @SuppressWarnings("resource")
   @Override
   protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> pOptions) {
-    Preconditions.checkState(!closed, "solver context is already closed");
+    Preconditions.checkState(!closed.get(), "solver context is already closed");
     return new BoolectorTheoremProver(
         manager, creator, creator.getEnv(), shutdownNotifier, pOptions, isAnyStackAlive);
   }

src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java

@@ -369,7 +369,6 @@ public List<? extends IExpression> parseStringToTerms(String s, PrincessFormulaC
    * Exception at run time.
    */
   @SuppressWarnings("unchecked")
-  @SuppressFBWarnings("THROWS_METHOD_THROWS_CLAUSE_THROWABLE")
   private static <E extends Throwable> void throwCheckedAsUnchecked(Throwable e) throws E {
     throw (E) e;
   }

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java

@@ -179,15 +179,6 @@ public Object convertValue(Term value) {
     }
   }
 
-  /** ApplicationTerms can be wrapped with "|". This function removes those chars. */
-  public static String dequote(String s) {
-    int l = s.length();
-    if (s.charAt(0) == '|' && s.charAt(l - 1) == '|') {
-      return s.substring(1, l - 1);
-    }
-    return s;
-  }
-
   @Override
   public <R> R visit(FormulaVisitor<R> visitor, Formula f, final Term input) {
     checkArgument(

src/org/sosy_lab/java_smt/solvers/z3/Z3SolverContext.java

@@ -17,6 +17,7 @@
 import java.nio.charset.StandardCharsets;
 import java.nio.file.Path;
 import java.util.Set;
+import java.util.concurrent.atomic.AtomicBoolean;
 import java.util.function.Consumer;
 import java.util.logging.Level;
 import org.checkerframework.checker.nullness.qual.Nullable;
@@ -46,7 +47,7 @@ public final class Z3SolverContext extends AbstractSolverContext {
   private final ExtraOptions extraOptions;
   private final Z3FormulaCreator creator;
   private final Z3FormulaManager manager;
-  private boolean closed = false;
+  private final AtomicBoolean closed = new AtomicBoolean(false);
 
   private static final String OPT_ENGINE_CONFIG_KEY = "optsmt_engine";
   private static final String OPT_PRIORITY_CONFIG_KEY = "priority";
@@ -215,7 +216,7 @@ public static synchronized Z3SolverContext create(
 
   @Override
   protected ProverEnvironment newProverEnvironment0(Set<ProverOptions> options) {
-    Preconditions.checkState(!closed, "solver context is already closed");
+    Preconditions.checkState(!closed.get(), "solver context is already closed");
     final ImmutableMap<String, Object> solverOptions =
         ImmutableMap.<String, Object>builder()
             .put(":random-seed", extraOptions.randomSeed)
@@ -241,7 +242,7 @@ protected InterpolatingProverEnvironment<?> newProverEnvironmentWithInterpolatio
   @Override
   public OptimizationProverEnvironment newOptimizationProverEnvironment0(
       Set<ProverOptions> options) {
-    Preconditions.checkState(!closed, "solver context is already closed");
+    Preconditions.checkState(!closed.get(), "solver context is already closed");
     final ImmutableMap<String, Object> solverOptions =
         ImmutableMap.<String, Object>builder()
             // .put(":random-seed", extraOptions.randomSeed) // not supported here
@@ -269,8 +270,7 @@ public Solvers getSolverName() {
 
   @Override
   public void close() {
-    if (!closed) {
-      closed = true;
+    if (!closed.getAndSet(true)) {
       long context = creator.getEnv();
       creator.forceClose();
       shutdownNotifier.unregister(interruptListener);

src/org/sosy_lab/java_smt/test/BooleanFormulaSubject.java

@@ -19,7 +19,6 @@
 import com.google.common.truth.StandardSubjectBuilder;
 import com.google.common.truth.Subject;
 import com.google.common.truth.Truth;
-import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.util.ArrayList;
 import java.util.List;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -39,7 +38,6 @@
  * {@link StandardSubjectBuilder#about(com.google.common.truth.Subject.Factory)} and set a solver
  * via the method {@link #booleanFormulasOf(SolverContext)}.
  */
-@SuppressFBWarnings("EQ_DOESNT_OVERRIDE_EQUALS")
 public final class BooleanFormulaSubject extends Subject {
 
   private final SolverContext context;

src/org/sosy_lab/java_smt/test/Fuzzer.java

@@ -8,7 +8,6 @@
 
 package org.sosy_lab.java_smt.test;
 
-import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.util.Random;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -42,7 +41,6 @@ public BooleanFormula fuzz(int formulaSize, BooleanFormula... pVars) {
     return recFuzz(formulaSize);
   }
 
-  @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE")
   private BooleanFormula recFuzz(int formulaSize) {
     if (formulaSize == 1) {
 
@@ -69,7 +67,6 @@ private BooleanFormula recFuzz(int formulaSize) {
     }
   }
 
-  @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE")
   private BooleanFormula getVar() {
     return vars[r.nextInt(vars.length)];
   }

src/org/sosy_lab/java_smt/test/IntegerTheoryFuzzer.java

@@ -8,7 +8,6 @@
 
 package org.sosy_lab.java_smt.test;
 
-import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.util.Random;
 import java.util.stream.IntStream;
 import org.sosy_lab.java_smt.api.FormulaManager;
@@ -43,7 +42,6 @@ public IntegerFormula fuzz(int formulaSize, int pMaxConstant, IntegerFormula...
     return recFuzz(formulaSize);
   }
 
-  @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE")
   private IntegerFormula recFuzz(int pFormulaSize) {
     if (pFormulaSize == 1) {
 
@@ -78,12 +76,10 @@ private IntegerFormula recFuzz(int pFormulaSize) {
     }
   }
 
-  @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE")
   private IntegerFormula getConstant() {
     return ifmgr.makeNumber((long) r.nextInt(2 * maxConstant) - maxConstant);
   }
 
-  @SuppressFBWarnings(value = "DMI_RANDOM_USED_ONLY_ONCE")
   private IntegerFormula getVar() {
     return vars[r.nextInt(vars.length)];
   }

src/org/sosy_lab/java_smt/test/ProverEnvironmentSubject.java

@@ -16,7 +16,6 @@
 import com.google.common.truth.FailureMetadata;
 import com.google.common.truth.StandardSubjectBuilder;
 import com.google.common.truth.Subject;
-import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.util.List;
 import org.sosy_lab.java_smt.api.BasicProverEnvironment;
 import org.sosy_lab.java_smt.api.BooleanFormula;
@@ -32,7 +31,6 @@
  * {@link StandardSubjectBuilder#about(com.google.common.truth.Subject.Factory)} and {@link
  * #proverEnvironments()}.
  */
-@SuppressFBWarnings("EQ_DOESNT_OVERRIDE_EQUALS")
 public final class ProverEnvironmentSubject extends Subject {
 
   private final BasicProverEnvironment<?> stackUnderTest;

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -14,7 +14,6 @@
 import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
 
 import com.google.common.truth.Truth;
-import edu.umd.cs.findbugs.annotations.SuppressFBWarnings;
 import java.util.Collection;
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.junit.After;
@@ -86,7 +85,6 @@
  * <p>Test that rely on a theory that not all solvers support should call one of the {@code require}
  * methods at the beginning.
  */
-@SuppressFBWarnings(value = "URF_UNREAD_PUBLIC_OR_PROTECTED_FIELD", justification = "test code")
 public abstract class SolverBasedTest0 {
 
   protected Configuration config;