Add Z3 implementation for prover based shutdown

Author: BaierD

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

@@ -25,6 +25,7 @@
 import java.util.Optional;
 import java.util.Set;
 import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.common.ShutdownManager;
 import org.sosy_lab.common.ShutdownNotifier;
 import org.sosy_lab.common.UniqueIdGenerator;
 import org.sosy_lab.common.collect.PathCopyingPersistentTreeMap;
@@ -261,4 +262,9 @@ public <R> R allSat(AllSatCallback<R> callback, List<BooleanFormula> important)
       throw creator.handleZ3Exception(e);
     }
   }
+
+  @Override
+  protected ShutdownManager getShutdownManagerForProverImpl() throws UnsupportedOperationException {
+    return proverShutdownManager;
+  }
 }

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

@@ -45,7 +45,7 @@ class Z3TheoremProver extends Z3AbstractProver implements ProverEnvironment {
     Native.solverIncRef(z3context, z3solver);
 
     interruptListener = reason -> Native.solverInterrupt(z3context, z3solver);
-    shutdownNotifier.register(interruptListener);
+    proverShutdownManager.getNotifier().register(interruptListener);
 
     long z3params = Native.mkParams(z3context);
     Native.paramsIncRef(z3context, z3params);
@@ -192,7 +192,7 @@ public void close() {
         propagator.close();
         propagator = null;
       }
-      shutdownNotifier.unregister(interruptListener);
+      proverShutdownManager.getNotifier().unregister(interruptListener);
     }
     super.close();
   }