Add more internal information about shutdown re-use for Z3 and Bitwuzla

Author: BaierD

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaTheoremProver.java

@@ -35,6 +35,9 @@
 import org.sosy_lab.java_smt.solvers.bitwuzla.api.Vector_Term;
 
 class BitwuzlaTheoremProver extends AbstractProverWithAllSat<Void> implements ProverEnvironment {
+
+  // Bitwuzlas termination is fully reusable. Even the terminated stack can be re-used. Confirmed
+  // by Mathias Preiner.
   private final Terminator terminator =
       new Terminator() {
         @Override

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

@@ -29,6 +29,9 @@
 class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment {
 
   private final long z3solver;
+
+  // Z3 interruption via solverInterrupt() is re-usable, but might provide partial results if it
+  // is stopping UnsatCore generation for example.
   private final ShutdownRequestListener interruptListener;
 
   private @Nullable Z3UserPropagator propagator = null;