Tests: provide separation logic as slmgr for tests.

Actually, there were never any tests for separation logic,
and nobody notices that is can not be used in current state.

Author: kfriedberger

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

@@ -47,6 +47,7 @@
 import org.sosy_lab.java_smt.api.ProverEnvironment;
 import org.sosy_lab.java_smt.api.QuantifiedFormulaManager;
 import org.sosy_lab.java_smt.api.RationalFormulaManager;
+import org.sosy_lab.java_smt.api.SLFormulaManager;
 import org.sosy_lab.java_smt.api.SolverContext;
 import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
 import org.sosy_lab.java_smt.api.SolverException;
@@ -104,6 +105,7 @@ public abstract class SolverBasedTest0 {
   protected @Nullable FloatingPointFormulaManager fpmgr;
   protected @Nullable StringFormulaManager smgr;
   protected @Nullable EnumerationFormulaManager emgr;
+  protected @Nullable SLFormulaManager slmgr;
   protected ShutdownManager shutdownManager = ShutdownManager.create();
 
   protected ShutdownNotifier shutdownNotifierToUse() {
@@ -192,6 +194,11 @@ public final void initSolver() throws InvalidConfigurationException {
     } catch (UnsupportedOperationException e) {
       emgr = null;
     }
+    try {
+      slmgr = mgr.getSLFormulaManager();
+    } catch (UnsupportedOperationException e) {
+      slmgr = null;
+    }
   }
 
   @After
@@ -306,6 +313,13 @@ protected final void requireEnumeration() {
         .isNotNull();
   }
 
+  protected final void requireSeparationLogic() {
+    assume()
+        .withMessage("Solver %s does not support the theory of separation logic", solverToUse())
+        .that(slmgr)
+        .isNotNull();
+  }
+
   /** Skip test if the solver does not support optimization. */
   protected final void requireOptimization() {
     try {