uuverifiers · johnynek · Feb 22, 2026 · Feb 22, 2026 · Feb 22, 2026 · Feb 22, 2026
diff --git a/build.sbt b/build.sbt
@@ -90,12 +90,28 @@ lazy val smtParser = (project in file("smt-parser")).
   ).
   disablePlugins(AssemblyPlugin)
 
+lazy val core = (project in file("core")).
+  settings(commonSettings: _*).
+  settings(
+    name := "Princess-core",
+    libraryDependencies +=
+      "org.scalacheck" %% "scalacheck" % "1.15.2" % Test,
+    Compile / scalacOptions ++=
+      List("-feature",
+           "-language:implicitConversions,postfixOps,reflectiveCalls"),
+    scalacOptions += (scalaVersion map { sv => sv match {
+      case "2.11.12" => "-optimise"
+      case "2.12.20" => "-opt:_"
+    }}).value
+  ).
+  disablePlugins(AssemblyPlugin)
+
 // Actual project
 
 lazy val root = (project in file(".")).
   enablePlugins(NativeImagePlugin).
-  aggregate(parser, smtParser).
-  dependsOn(parser, smtParser).
+  aggregate(core, parser, smtParser).
+  dependsOn(core, parser, smtParser).
   settings(commonSettings: _*).
 //
   settings(
@@ -129,4 +145,3 @@ lazy val root = (project in file(".")).
 
     nativeImageAgentMerge := true
 )
-
diff --git a/src/main/scala/ap/PresburgerTools.scala → core/src/main/scala/ap/PresburgerTools.scala b/src/main/scala/ap/PresburgerTools.scala → core/src/main/scala/ap/PresburgerTools.scala
diff --git a/src/main/scala/ap/Prover.scala → core/src/main/scala/ap/Prover.scala b/src/main/scala/ap/Prover.scala → core/src/main/scala/ap/Prover.scala
diff --git a/src/main/scala/ap/Signature.scala → core/src/main/scala/ap/Signature.scala b/src/main/scala/ap/Signature.scala → core/src/main/scala/ap/Signature.scala
diff --git a/src/main/scala/ap/algebra/Group.scala → core/src/main/scala/ap/algebra/Group.scala b/src/main/scala/ap/algebra/Group.scala → core/src/main/scala/ap/algebra/Group.scala
diff --git a/src/main/scala/ap/algebra/Integers.scala → .../src/main/scala/ap/algebra/Integers.scala b/src/main/scala/ap/algebra/Integers.scala → .../src/main/scala/ap/algebra/Integers.scala
diff --git a/src/main/scala/ap/algebra/Ring.scala → core/src/main/scala/ap/algebra/Ring.scala b/src/main/scala/ap/algebra/Ring.scala → core/src/main/scala/ap/algebra/Ring.scala
diff --git a/src/main/scala/ap/algebra/package.scala → core/src/main/scala/ap/algebra/package.scala b/src/main/scala/ap/algebra/package.scala → core/src/main/scala/ap/algebra/package.scala
diff --git a/src/main/scala/ap/api/PartialModel.scala → .../src/main/scala/ap/api/PartialModel.scala b/src/main/scala/ap/api/PartialModel.scala → .../src/main/scala/ap/api/PartialModel.scala
diff --git a/...in/scala/ap/basetypes/HeapCollector.scala → ...in/scala/ap/basetypes/HeapCollector.scala b/...in/scala/ap/basetypes/HeapCollector.scala → ...in/scala/ap/basetypes/HeapCollector.scala
diff --git a/src/main/scala/ap/basetypes/IdealInt.scala → ...rc/main/scala/ap/basetypes/IdealInt.scala b/src/main/scala/ap/basetypes/IdealInt.scala → ...rc/main/scala/ap/basetypes/IdealInt.scala
diff --git a/src/main/scala/ap/basetypes/IdealRat.scala → ...rc/main/scala/ap/basetypes/IdealRat.scala b/src/main/scala/ap/basetypes/IdealRat.scala → ...rc/main/scala/ap/basetypes/IdealRat.scala
diff --git a/...main/scala/ap/basetypes/LeftistHeap.scala → ...main/scala/ap/basetypes/LeftistHeap.scala b/...main/scala/ap/basetypes/LeftistHeap.scala → ...main/scala/ap/basetypes/LeftistHeap.scala
diff --git a/src/main/scala/ap/basetypes/MultiSet.scala → ...rc/main/scala/ap/basetypes/MultiSet.scala b/src/main/scala/ap/basetypes/MultiSet.scala → ...rc/main/scala/ap/basetypes/MultiSet.scala
diff --git a/src/main/scala/ap/basetypes/SetTrie.scala → ...src/main/scala/ap/basetypes/SetTrie.scala b/src/main/scala/ap/basetypes/SetTrie.scala → ...src/main/scala/ap/basetypes/SetTrie.scala
diff --git a/src/main/scala/ap/basetypes/Tree.scala → core/src/main/scala/ap/basetypes/Tree.scala b/src/main/scala/ap/basetypes/Tree.scala → core/src/main/scala/ap/basetypes/Tree.scala
diff --git a/src/main/scala/ap/basetypes/UnionFind.scala → ...c/main/scala/ap/basetypes/UnionFind.scala b/src/main/scala/ap/basetypes/UnionFind.scala → ...c/main/scala/ap/basetypes/UnionFind.scala
diff --git a/core/src/main/scala/ap/core/ImplicationChecker.scala b/core/src/main/scala/ap/core/ImplicationChecker.scala
@@ -0,0 +1,23 @@
+package ap.core
+
+import ap.PresburgerTools
+import ap.parser.{IFormula, IExpression, SymbolCollector, InputAbsy2Internal, IBoolLit}
+import ap.terfor.TermOrder
+import ap.terfor.conjunctions.Conjunction
+
+object ImplicationChecker {
+
+  import IExpression._
+
+  def implies(assumptions : Seq[IFormula], conclusion : IFormula) : Boolean = {
+    val premise = assumptions.foldLeft[IFormula](IBoolLit(true))(_ & _)
+    isValid(premise ==> conclusion)
+  }
+
+  def isValid(formula : IFormula) : Boolean = {
+    val order =
+      TermOrder.EMPTY.extend(SymbolCollector.constantsSorted(formula))
+    val internal = InputAbsy2Internal(formula, order)
+    PresburgerTools.isValid(Conjunction.conj(internal, order))
+  }
+}
diff --git a/...in/scala/ap/interpolants/BenchUtils.scala → ...in/scala/ap/interpolants/BenchUtils.scala b/...in/scala/ap/interpolants/BenchUtils.scala → ...in/scala/ap/interpolants/BenchUtils.scala
diff --git a/.../interpolants/InterpolantSimplifier.scala → .../interpolants/InterpolantSimplifier.scala b/.../interpolants/InterpolantSimplifier.scala → .../interpolants/InterpolantSimplifier.scala
diff --git a/...p/interpolants/InterpolationContext.scala → ...p/interpolants/InterpolationContext.scala b/...p/interpolants/InterpolationContext.scala → ...p/interpolants/InterpolationContext.scala
diff --git a/.../scala/ap/interpolants/Interpolator.scala → .../scala/ap/interpolants/Interpolator.scala b/.../scala/ap/interpolants/Interpolator.scala → .../scala/ap/interpolants/Interpolator.scala
diff --git a/...cala/ap/interpolants/InterpolatorQE.scala → ...cala/ap/interpolants/InterpolatorQE.scala b/...cala/ap/interpolants/InterpolatorQE.scala → ...cala/ap/interpolants/InterpolatorQE.scala
diff --git a/.../ap/interpolants/PartialInterpolant.scala → .../ap/interpolants/PartialInterpolant.scala b/.../ap/interpolants/PartialInterpolant.scala → .../ap/interpolants/PartialInterpolant.scala
diff --git a/...ala/ap/interpolants/ProofSimplifier.scala → ...ala/ap/interpolants/ProofSimplifier.scala b/...ala/ap/interpolants/ProofSimplifier.scala → ...ala/ap/interpolants/ProofSimplifier.scala
diff --git a/src/main/scala/ap/parameters/Param.scala → .../src/main/scala/ap/parameters/Param.scala b/src/main/scala/ap/parameters/Param.scala → .../src/main/scala/ap/parameters/Param.scala
diff --git a/src/main/scala/ap/parameters/Settings.scala → ...c/main/scala/ap/parameters/Settings.scala b/src/main/scala/ap/parameters/Settings.scala → ...c/main/scala/ap/parameters/Settings.scala
diff --git a/...scala/ap/parser/BooleanCompactifier.scala → ...scala/ap/parser/BooleanCompactifier.scala b/...scala/ap/parser/BooleanCompactifier.scala → ...scala/ap/parser/BooleanCompactifier.scala
diff --git a/...in/scala/ap/parser/CSIsatLineariser.scala → ...in/scala/ap/parser/CSIsatLineariser.scala b/...in/scala/ap/parser/CSIsatLineariser.scala → ...in/scala/ap/parser/CSIsatLineariser.scala
diff --git a/src/main/scala/ap/parser/Environment.scala → ...rc/main/scala/ap/parser/Environment.scala b/src/main/scala/ap/parser/Environment.scala → ...rc/main/scala/ap/parser/Environment.scala
diff --git a/src/main/scala/ap/parser/EquivExpander.scala → .../main/scala/ap/parser/EquivExpander.scala b/src/main/scala/ap/parser/EquivExpander.scala → .../main/scala/ap/parser/EquivExpander.scala
diff --git a/src/main/scala/ap/parser/EquivInliner.scala → ...c/main/scala/ap/parser/EquivInliner.scala b/src/main/scala/ap/parser/EquivInliner.scala → ...c/main/scala/ap/parser/EquivInliner.scala
diff --git a/src/main/scala/ap/parser/ExMaxiscoper.scala → ...c/main/scala/ap/parser/ExMaxiscoper.scala b/src/main/scala/ap/parser/ExMaxiscoper.scala → ...c/main/scala/ap/parser/ExMaxiscoper.scala
diff --git a/...ain/scala/ap/parser/FunctionEncoder.scala → ...ain/scala/ap/parser/FunctionEncoder.scala b/...ain/scala/ap/parser/FunctionEncoder.scala → ...ain/scala/ap/parser/FunctionEncoder.scala
diff --git a/...ala/ap/parser/FunctionPreprocessing.scala → ...ala/ap/parser/FunctionPreprocessing.scala b/...ala/ap/parser/FunctionPreprocessing.scala → ...ala/ap/parser/FunctionPreprocessing.scala
diff --git a/src/main/scala/ap/parser/IExpression.scala → ...rc/main/scala/ap/parser/IExpression.scala b/src/main/scala/ap/parser/IExpression.scala → ...rc/main/scala/ap/parser/IExpression.scala
diff --git a/src/main/scala/ap/parser/IFormula.scala → core/src/main/scala/ap/parser/IFormula.scala b/src/main/scala/ap/parser/IFormula.scala → core/src/main/scala/ap/parser/IFormula.scala
diff --git a/src/main/scala/ap/parser/ITerm.scala → core/src/main/scala/ap/parser/ITerm.scala b/src/main/scala/ap/parser/ITerm.scala → core/src/main/scala/ap/parser/ITerm.scala
diff --git a/...ala/ap/parser/ImplicationCompressor.scala → ...ala/ap/parser/ImplicationCompressor.scala b/...ala/ap/parser/ImplicationCompressor.scala → ...ala/ap/parser/ImplicationCompressor.scala
diff --git a/.../scala/ap/parser/InputAbsy2Internal.scala → .../scala/ap/parser/InputAbsy2Internal.scala b/.../scala/ap/parser/InputAbsy2Internal.scala → .../scala/ap/parser/InputAbsy2Internal.scala
diff --git a/...in/scala/ap/parser/InputAbsyVisitor.scala → ...in/scala/ap/parser/InputAbsyVisitor.scala b/...in/scala/ap/parser/InputAbsyVisitor.scala → ...in/scala/ap/parser/InputAbsyVisitor.scala
diff --git a/.../scala/ap/parser/Internal2InputAbsy.scala → .../scala/ap/parser/Internal2InputAbsy.scala b/.../scala/ap/parser/Internal2InputAbsy.scala → .../scala/ap/parser/Internal2InputAbsy.scala
diff --git a/src/main/scala/ap/parser/KBO.scala → core/src/main/scala/ap/parser/KBO.scala b/src/main/scala/ap/parser/KBO.scala → core/src/main/scala/ap/parser/KBO.scala
diff --git a/...in/scala/ap/parser/Parser2InputAbsy.scala → ...in/scala/ap/parser/Parser2InputAbsy.scala b/...in/scala/ap/parser/Parser2InputAbsy.scala → ...in/scala/ap/parser/Parser2InputAbsy.scala
diff --git a/src/main/scala/ap/parser/PartExtractor.scala → .../main/scala/ap/parser/PartExtractor.scala b/src/main/scala/ap/parser/PartExtractor.scala → .../main/scala/ap/parser/PartExtractor.scala
diff --git a/...in/scala/ap/parser/PartialEvaluator.scala → ...in/scala/ap/parser/PartialEvaluator.scala b/...in/scala/ap/parser/PartialEvaluator.scala → ...in/scala/ap/parser/PartialEvaluator.scala
diff --git a/...main/scala/ap/parser/Postprocessing.scala → ...main/scala/ap/parser/Postprocessing.scala b/...main/scala/ap/parser/Postprocessing.scala → ...main/scala/ap/parser/Postprocessing.scala
diff --git a/src/main/scala/ap/parser/Preprocessing.scala → .../main/scala/ap/parser/Preprocessing.scala b/src/main/scala/ap/parser/Preprocessing.scala → .../main/scala/ap/parser/Preprocessing.scala
diff --git a/src/main/scala/ap/parser/Rewriter.scala → core/src/main/scala/ap/parser/Rewriter.scala b/src/main/scala/ap/parser/Rewriter.scala → core/src/main/scala/ap/parser/Rewriter.scala
diff --git a/src/main/scala/ap/parser/SMTLineariser.scala → .../main/scala/ap/parser/SMTLineariser.scala b/src/main/scala/ap/parser/SMTLineariser.scala → .../main/scala/ap/parser/SMTLineariser.scala
@@ -61,7 +61,7 @@ import java.io.PrintStream
 object SMTLineariser {
 
   import SMTTypes._
-  import SMTParser2InputAbsy.SMTFunctionType
+  import SMTSupport.SMTFunctionType
 
   private val AC = Debug.AC_PARSER
 
@@ -631,9 +631,9 @@ object SMTLineariser {
             constantType :
               ConstantTerm => Option[SMTTypes.SMTType],
             functionType :
-              IFunction => Option[SMTParser2InputAbsy.SMTFunctionType],
+              IFunction => Option[SMTSupport.SMTFunctionType],
             predType :
-              Predicate => Option[SMTParser2InputAbsy.SMTFunctionType],
+              Predicate => Option[SMTSupport.SMTFunctionType],
             prettyBitvectors : Boolean = true) : Unit =
     formula match {
       case IBoolLit(value) => print(value)
@@ -671,11 +671,21 @@ object SMTLineariser {
     case t : ITerm => asString(t)
   }
 
+  private def captureString(comp : => Unit) : String = {
+    val out = new java.io.ByteArrayOutputStream
+    val ps = new java.io.PrintStream(out)
+    Console.withOut(ps) {
+      comp
+    }
+    ps.flush()
+    out.toString("UTF-8")
+  }
+
   def asString(formula : IFormula) : String =
-    ap.DialogUtil.asString { apply(formula) }
+    captureString { apply(formula) }
 
   def asString(t : ITerm) : String =
-    ap.DialogUtil.asString { apply(t) }
+    captureString { apply(t) }
 
   //////////////////////////////////////////////////////////////////////////////
 
@@ -946,9 +956,9 @@ class SMTLineariser(benchmarkName     : String,
                     constantType :
                        ConstantTerm => Option[SMTTypes.SMTType],
                     functionType :
-                       IFunction => Option[SMTParser2InputAbsy.SMTFunctionType],
+                       IFunction => Option[SMTSupport.SMTFunctionType],
                     predType :
-                       Predicate => Option[SMTParser2InputAbsy.SMTFunctionType],
+                       Predicate => Option[SMTSupport.SMTFunctionType],
                     prettyBitvectors : Boolean = true) {
 
   import SMTTypes._
@@ -1065,7 +1075,7 @@ class SMTLineariser(benchmarkName     : String,
 
   //////////////////////////////////////////////////////////////////////////////
 
-  import SMTParser2InputAbsy.SMTFunctionType
+  import SMTSupport.SMTFunctionType
 
   private def getTermType(t : ITerm)
                          (implicit variableType : Int => Option[SMTType])
@@ -1484,4 +1494,3 @@ class SMTLineariser(benchmarkName     : String,
   }
 
 }
-
diff --git a/.../scala/ap/parser/SMTParseableTheory.scala → .../scala/ap/parser/SMTParseableTheory.scala b/.../scala/ap/parser/SMTParseableTheory.scala → .../scala/ap/parser/SMTParseableTheory.scala
@@ -34,7 +34,6 @@
 package ap.parser
 
 import ap.theories.Theory
-import ap.parser.smtlib.Absyn.{Sort => SSort, SymbolRef}
 import ap.types.Sort
 
 /**
@@ -89,18 +88,21 @@ trait SMTParseableTheory {
 
   import SMTTypes.SMTType
 
+  type SMTSortAST = Any
+  type SMTSymbolRefAST = Any
+
   /**
    * Translate a sort AST.
    */
-  def translateSMTSortAST(s : SSort) : Option[SMTType] = None
+  def translateSMTSortAST(s : SMTSortAST) : Option[SMTType] = None
 
   /**
    * Translate the application of a function or predicate. The
    * arguments can be translated recursively, given their polarity as
    * argument.
    */
   def translateSMTOperatorAST(
-          sym       : SymbolRef,
+          sym       : SMTSymbolRefAST,
           arguments : Seq[(Int) => (IExpression, SMTType)],
           polarity  : Int)
                     : Option[(IExpression, SMTType)] = None

diff --git a/core/src/main/scala/ap/parser/SMTSupport.scala b/core/src/main/scala/ap/parser/SMTSupport.scala
@@ -0,0 +1,21 @@
+/**
+ * Shared SMT helper types that are independent from concrete frontends.
+ */
+package ap.parser
+
+object SMTSupport {
+
+  import IExpression.{Sort => TSort}
+  import SMTTypes._
+
+  def toNormalBool(s : TSort) : TSort = s match {
+    case TSort.MultipleValueBool => TSort.Bool
+    case other                   => other
+  }
+
+  case class SMTFunctionType(arguments : List[SMTType],
+                             result : SMTType)
+
+  val SMTBoolVariableType : SMTFunctionType =
+    SMTFunctionType(List(), SMTBool)
+}
diff --git a/src/main/scala/ap/parser/SMTTypes.scala → core/src/main/scala/ap/parser/SMTTypes.scala b/src/main/scala/ap/parser/SMTTypes.scala → core/src/main/scala/ap/parser/SMTTypes.scala
@@ -34,7 +34,6 @@
 package ap.parser;
 
 import ap.basetypes.IdealInt
-import ap.DialogUtil
 import ap.types.Sort
 import ap.theories.{ADT, ModuloArithmetic, TheoryRegistry}
 import ap.theories.sequences.SeqTheory
@@ -53,7 +52,17 @@ object SMTTypes {
 
   private val AC = Debug.AC_PARSER
 
-  import SMTParser2InputAbsy.toNormalBool
+  import SMTSupport.toNormalBool
+
+  private def asString(comp : => Unit) : String = {
+    val out = new java.io.ByteArrayOutputStream
+    val ps = new java.io.PrintStream(out)
+    Console.withOut(ps) {
+      comp
+    }
+    ps.flush()
+    out.toString("UTF-8")
+  }
 
   abstract class SMTType {
     def toSort : Sort
@@ -80,7 +89,7 @@ object SMTTypes {
     val theory = ExtArray(arguments map { t => toNormalBool(t.toSort) },
                           toNormalBool(result.toSort))
     def toSort = theory.sort
-    def toSMTLIBString = DialogUtil asString {
+    def toSMTLIBString = asString {
       print("(Array")
       for (s <- arguments) {
         print(" ")
@@ -190,7 +199,7 @@ object SMTTypes {
                     elementType : SMTType)         extends SMTType {
     def toSort = theory.sort
     override def toString = theory.toString
-    def toSMTLIBString = DialogUtil asString {
+    def toSMTLIBString = asString {
       print("(Seq ")
       print(elementType.toSMTLIBString)
       print(")")

diff --git a/...in/scala/ap/parser/SimpleClausifier.scala → ...in/scala/ap/parser/SimpleClausifier.scala b/...in/scala/ap/parser/SimpleClausifier.scala → ...in/scala/ap/parser/SimpleClausifier.scala
diff --git a/...in/scala/ap/parser/SimpleMiniscoper.scala → ...in/scala/ap/parser/SimpleMiniscoper.scala b/...in/scala/ap/parser/SimpleMiniscoper.scala → ...in/scala/ap/parser/SimpleMiniscoper.scala
diff --git a/src/main/scala/ap/parser/Simplifier.scala → ...src/main/scala/ap/parser/Simplifier.scala b/src/main/scala/ap/parser/Simplifier.scala → ...src/main/scala/ap/parser/Simplifier.scala
diff --git a/...main/scala/ap/parser/TPTPLineariser.scala → ...main/scala/ap/parser/TPTPLineariser.scala b/...main/scala/ap/parser/TPTPLineariser.scala → ...main/scala/ap/parser/TPTPLineariser.scala
diff --git a/...in/scala/ap/parser/TriggerGenerator.scala → ...in/scala/ap/parser/TriggerGenerator.scala b/...in/scala/ap/parser/TriggerGenerator.scala → ...in/scala/ap/parser/TriggerGenerator.scala
diff --git a/src/main/scala/ap/proof/BindingContext.scala → .../main/scala/ap/proof/BindingContext.scala b/src/main/scala/ap/proof/BindingContext.scala → .../main/scala/ap/proof/BindingContext.scala
diff --git a/...main/scala/ap/proof/ConstantFreedom.scala → ...main/scala/ap/proof/ConstantFreedom.scala b/...main/scala/ap/proof/ConstantFreedom.scala → ...main/scala/ap/proof/ConstantFreedom.scala
diff --git a/...scala/ap/proof/ConstraintSimplifier.scala → ...scala/ap/proof/ConstraintSimplifier.scala b/...scala/ap/proof/ConstraintSimplifier.scala → ...scala/ap/proof/ConstraintSimplifier.scala
@@ -93,6 +93,11 @@ abstract class ConstraintSimplifier {
 
 class SimpleSimplifier(lemmas : Boolean, ground2DNF : Boolean, output : Boolean)
       extends ConstraintSimplifier {
+
+  private val NullStream =
+    new java.io.PrintStream(new java.io.OutputStream {
+      def write(b : Int) : Unit = ()
+    })
 
   private lazy val posProver =
     new ExhaustiveProver(false,
@@ -155,10 +160,10 @@ class SimpleSimplifier(lemmas : Boolean, ground2DNF : Boolean, output : Boolean)
   private def simplify(f : Conjunction, order : TermOrder) : Conjunction =
     Timeout.unfinishedValue(None) {
       println("Simplify: " + f + " (positive)")
-      val res = if (lemmas) Console.withOut(ap.CmdlMain.NullStream) {
+      val res = if (lemmas) Console.withOut(NullStream) {
         QuantifierElimProver(f, false, order)
       } else {
-        val tree = Console.withOut(ap.CmdlMain.NullStream) { posProver(f, order) }
+        val tree = Console.withOut(NullStream) { posProver(f, order) }
         TestProofTree.assertNormalisedTree(tree)
         tree.closingConstraint
       }
@@ -169,10 +174,10 @@ class SimpleSimplifier(lemmas : Boolean, ground2DNF : Boolean, output : Boolean)
   private def negSimplify(f : Conjunction, order : TermOrder) : Conjunction =
     Timeout.unfinishedValue(None) {
       println("Simplify: " + f + " (negative)")
-      val res = if (lemmas) Console.withOut(ap.CmdlMain.NullStream) {
+      val res = if (lemmas) Console.withOut(NullStream) {
         QuantifierElimProver(f.negate, ground2DNF, order).negate
       } else {
-        val tree = Console.withOut(ap.CmdlMain.NullStream) { negProver(f.negate, order) }
+        val tree = Console.withOut(NullStream) { negProver(f.negate, order) }
         TestProofTree.assertNormalisedTree(tree)
         tree.closingConstraint.negate
       }

diff --git a/...ain/scala/ap/proof/ExhaustiveProver.scala → ...ain/scala/ap/proof/ExhaustiveProver.scala b/...ain/scala/ap/proof/ExhaustiveProver.scala → ...ain/scala/ap/proof/ExhaustiveProver.scala
diff --git a/...in/scala/ap/proof/ModelSearchProver.scala → ...in/scala/ap/proof/ModelSearchProver.scala b/...in/scala/ap/proof/ModelSearchProver.scala → ...in/scala/ap/proof/ModelSearchProver.scala
@@ -326,53 +326,9 @@ class ModelSearchProver(defaultSettings : GoalSettings) {
   //////////////////////////////////////////////////////////////////////////////
 
   private def verifyCertificate(cert : Certificate,
-                                disjuncts : Seq[Conjunction]) : Boolean = {
-
-    // verify assumptions
-    (cert.assumedFormulas subsetOf
-      (for (d <- disjuncts.iterator) yield CertFormula(d.negate)).toSet) &&
-    //
-    // verify theory axioms
-    (true || SimpleAPI.withProver { p =>
-      import p._
-
-      def traverse(c : Certificate) : Boolean =
-        (c match {
-          case BranchInferenceCertificate(inferences, _, order) =>
-            inferences forall {
-              case TheoryAxiomInference(axiom, GroebnerMultiplication) =>
-                scope {
-                  Console.err.println("Verifying: " + axiom)
-                  addTheory(GroebnerMultiplication)
-                  addConclusion(axiom.toConj)
-
-                  try {
-                    withTimeout(3000) {
-                      ??? match {
-                        case SimpleAPI.ProverStatus.Valid =>
-                          true
-                        case _ =>
-                          Console.err.println("FAILED")
-                          true
-                      }
-                    }
-                  } catch {
-                    case SimpleAPI.TimeoutException =>
-                      Console.err.println("T/O")
-                      true
-                  }
-                }
-              case _ =>
-                true
-            }
-          case _ =>
-            true
-         }) &&
-        (c.subCertificates forall (traverse _))
-
-      traverse(cert)
-    })
-  }
+                                disjuncts : Seq[Conjunction]) : Boolean =
+    cert.assumedFormulas subsetOf
+      (for (d <- disjuncts.iterator) yield CertFormula(d.negate)).toSet
 
   //////////////////////////////////////////////////////////////////////////////
 

diff --git a/...scala/ap/proof/QuantifierElimProver.scala → ...scala/ap/proof/QuantifierElimProver.scala b/...scala/ap/proof/QuantifierElimProver.scala → ...scala/ap/proof/QuantifierElimProver.scala
diff --git a/src/main/scala/ap/proof/Vocabulary.scala → .../src/main/scala/ap/proof/Vocabulary.scala b/src/main/scala/ap/proof/Vocabulary.scala → .../src/main/scala/ap/proof/Vocabulary.scala
diff --git a/...roof/certificates/BinaryCertificate.scala → ...roof/certificates/BinaryCertificate.scala b/...roof/certificates/BinaryCertificate.scala → ...roof/certificates/BinaryCertificate.scala
diff --git a/...tificates/BranchInferenceCollection.scala → ...tificates/BranchInferenceCollection.scala b/...tificates/BranchInferenceCollection.scala → ...tificates/BranchInferenceCollection.scala
diff --git a/...a/ap/proof/certificates/CertFormula.scala → ...a/ap/proof/certificates/CertFormula.scala b/...a/ap/proof/certificates/CertFormula.scala → ...a/ap/proof/certificates/CertFormula.scala
diff --git a/...a/ap/proof/certificates/Certificate.scala → ...a/ap/proof/certificates/Certificate.scala b/...a/ap/proof/certificates/Certificate.scala → ...a/ap/proof/certificates/Certificate.scala
diff --git a/...of/certificates/CertificateOneChild.scala → ...of/certificates/CertificateOneChild.scala b/...of/certificates/CertificateOneChild.scala → ...of/certificates/CertificateOneChild.scala
diff --git a/...proof/certificates/CloseCertificate.scala → ...proof/certificates/CloseCertificate.scala b/...proof/certificates/CloseCertificate.scala → ...proof/certificates/CloseCertificate.scala
diff --git a/...ertificates/DagCertificateConverter.scala → ...ertificates/DagCertificateConverter.scala b/...ertificates/DagCertificateConverter.scala → ...ertificates/DagCertificateConverter.scala
diff --git a/...ap/proof/certificates/DotLineariser.scala → ...ap/proof/certificates/DotLineariser.scala b/...ap/proof/certificates/DotLineariser.scala → ...ap/proof/certificates/DotLineariser.scala
diff --git a/...ala/ap/proof/certificates/LemmaBase.scala → ...ala/ap/proof/certificates/LemmaBase.scala b/...ala/ap/proof/certificates/LemmaBase.scala → ...ala/ap/proof/certificates/LemmaBase.scala
diff --git a/...proof/certificates/OmegaCertificate.scala → ...proof/certificates/OmegaCertificate.scala b/...proof/certificates/OmegaCertificate.scala → ...proof/certificates/OmegaCertificate.scala
diff --git a/.../proof/certificates/PropCertificate.scala → .../proof/certificates/PropCertificate.scala b/.../proof/certificates/PropCertificate.scala → .../proof/certificates/PropCertificate.scala
diff --git a/...oof/certificates/SplitEqCertificate.scala → ...oof/certificates/SplitEqCertificate.scala b/...oof/certificates/SplitEqCertificate.scala → ...oof/certificates/SplitEqCertificate.scala
diff --git a/.../certificates/StrengthenCertificate.scala → .../certificates/StrengthenCertificate.scala b/.../certificates/StrengthenCertificate.scala → .../certificates/StrengthenCertificate.scala
diff --git a/...in/scala/ap/proof/goal/AddFactsTask.scala → ...in/scala/ap/proof/goal/AddFactsTask.scala b/...in/scala/ap/proof/goal/AddFactsTask.scala → ...in/scala/ap/proof/goal/AddFactsTask.scala
diff --git a/...n/scala/ap/proof/goal/AliasAnalyser.scala → ...n/scala/ap/proof/goal/AliasAnalyser.scala b/...n/scala/ap/proof/goal/AliasAnalyser.scala → ...n/scala/ap/proof/goal/AliasAnalyser.scala
diff --git a/...ala/ap/proof/goal/AllQuantifierTask.scala → ...ala/ap/proof/goal/AllQuantifierTask.scala b/...ala/ap/proof/goal/AllQuantifierTask.scala → ...ala/ap/proof/goal/AllQuantifierTask.scala
diff --git a/...scala/ap/proof/goal/BetaFormulaTask.scala → ...scala/ap/proof/goal/BetaFormulaTask.scala b/...scala/ap/proof/goal/BetaFormulaTask.scala → ...scala/ap/proof/goal/BetaFormulaTask.scala
diff --git a/...la/ap/proof/goal/BlockedFormulaTask.scala → ...la/ap/proof/goal/BlockedFormulaTask.scala b/...la/ap/proof/goal/BlockedFormulaTask.scala → ...la/ap/proof/goal/BlockedFormulaTask.scala
diff --git a/...a/ap/proof/goal/BoundStrengthenTask.scala → ...a/ap/proof/goal/BoundStrengthenTask.scala b/...a/ap/proof/goal/BoundStrengthenTask.scala → ...a/ap/proof/goal/BoundStrengthenTask.scala
diff --git a/...cala/ap/proof/goal/CompoundFormulas.scala → ...cala/ap/proof/goal/CompoundFormulas.scala b/...cala/ap/proof/goal/CompoundFormulas.scala → ...cala/ap/proof/goal/CompoundFormulas.scala
diff --git a/...cala/ap/proof/goal/DivisibilityTask.scala → ...cala/ap/proof/goal/DivisibilityTask.scala b/...cala/ap/proof/goal/DivisibilityTask.scala → ...cala/ap/proof/goal/DivisibilityTask.scala
diff --git a/src/main/scala/ap/proof/goal/EagerTask.scala → .../main/scala/ap/proof/goal/EagerTask.scala b/src/main/scala/ap/proof/goal/EagerTask.scala → .../main/scala/ap/proof/goal/EagerTask.scala
diff --git a/...cala/ap/proof/goal/EagerTaskManager.scala → ...cala/ap/proof/goal/EagerTaskManager.scala b/...cala/ap/proof/goal/EagerTaskManager.scala → ...cala/ap/proof/goal/EagerTaskManager.scala
diff --git a/...la/ap/proof/goal/EliminateFactsTask.scala → ...la/ap/proof/goal/EliminateFactsTask.scala b/...la/ap/proof/goal/EliminateFactsTask.scala → ...la/ap/proof/goal/EliminateFactsTask.scala
diff --git a/...cala/ap/proof/goal/ExQuantifierTask.scala → ...cala/ap/proof/goal/ExQuantifierTask.scala b/...cala/ap/proof/goal/ExQuantifierTask.scala → ...cala/ap/proof/goal/ExQuantifierTask.scala
diff --git a/...p/proof/goal/FactsNormalisationTask.scala → ...p/proof/goal/FactsNormalisationTask.scala b/...p/proof/goal/FactsNormalisationTask.scala → ...p/proof/goal/FactsNormalisationTask.scala
diff --git a/...ain/scala/ap/proof/goal/FormulaTask.scala → ...ain/scala/ap/proof/goal/FormulaTask.scala b/...ain/scala/ap/proof/goal/FormulaTask.scala → ...ain/scala/ap/proof/goal/FormulaTask.scala
diff --git a/src/main/scala/ap/proof/goal/Goal.scala → core/src/main/scala/ap/proof/goal/Goal.scala b/src/main/scala/ap/proof/goal/Goal.scala → core/src/main/scala/ap/proof/goal/Goal.scala
diff --git a/...main/scala/ap/proof/goal/MatchTasks.scala → ...main/scala/ap/proof/goal/MatchTasks.scala b/...main/scala/ap/proof/goal/MatchTasks.scala → ...main/scala/ap/proof/goal/MatchTasks.scala
diff --git a/...cala/ap/proof/goal/NegLitClauseTask.scala → ...cala/ap/proof/goal/NegLitClauseTask.scala b/...cala/ap/proof/goal/NegLitClauseTask.scala → ...cala/ap/proof/goal/NegLitClauseTask.scala
diff --git a/src/main/scala/ap/proof/goal/OmegaTask.scala → .../main/scala/ap/proof/goal/OmegaTask.scala b/src/main/scala/ap/proof/goal/OmegaTask.scala → .../main/scala/ap/proof/goal/OmegaTask.scala
diff --git a/...scala/ap/proof/goal/PrioritisedTask.scala → ...scala/ap/proof/goal/PrioritisedTask.scala b/...scala/ap/proof/goal/PrioritisedTask.scala → ...scala/ap/proof/goal/PrioritisedTask.scala
diff --git a/.../scala/ap/proof/goal/QuantifierTask.scala → .../scala/ap/proof/goal/QuantifierTask.scala b/.../scala/ap/proof/goal/QuantifierTask.scala → .../scala/ap/proof/goal/QuantifierTask.scala
diff --git a/...n/scala/ap/proof/goal/SymbolWeigths.scala → ...n/scala/ap/proof/goal/SymbolWeigths.scala b/...n/scala/ap/proof/goal/SymbolWeigths.scala → ...n/scala/ap/proof/goal/SymbolWeigths.scala
diff --git a/src/main/scala/ap/proof/goal/Task.scala → core/src/main/scala/ap/proof/goal/Task.scala b/src/main/scala/ap/proof/goal/Task.scala → core/src/main/scala/ap/proof/goal/Task.scala
diff --git a/.../scala/ap/proof/goal/TaskAggregator.scala → .../scala/ap/proof/goal/TaskAggregator.scala b/.../scala/ap/proof/goal/TaskAggregator.scala → .../scala/ap/proof/goal/TaskAggregator.scala
diff --git a/...ain/scala/ap/proof/goal/TaskManager.scala → ...ain/scala/ap/proof/goal/TaskManager.scala b/...ain/scala/ap/proof/goal/TaskManager.scala → ...ain/scala/ap/proof/goal/TaskManager.scala
diff --git a/...roof/goal/UpdateConstantFreedomTask.scala → ...roof/goal/UpdateConstantFreedomTask.scala b/...roof/goal/UpdateConstantFreedomTask.scala → ...roof/goal/UpdateConstantFreedomTask.scala
diff --git a/...scala/ap/proof/goal/UpdateTasksTask.scala → ...scala/ap/proof/goal/UpdateTasksTask.scala b/...scala/ap/proof/goal/UpdateTasksTask.scala → ...scala/ap/proof/goal/UpdateTasksTask.scala
diff --git a/...la/ap/proof/goal/WrappedFormulaTask.scala → ...la/ap/proof/goal/WrappedFormulaTask.scala b/...la/ap/proof/goal/WrappedFormulaTask.scala → ...la/ap/proof/goal/WrappedFormulaTask.scala
diff --git a/...scala/ap/proof/theoryPlugins/Plugin.scala → ...scala/ap/proof/theoryPlugins/Plugin.scala b/...scala/ap/proof/theoryPlugins/Plugin.scala → ...scala/ap/proof/theoryPlugins/Plugin.scala
diff --git a/src/main/scala/ap/proof/tree/AndTree.scala → ...rc/main/scala/ap/proof/tree/AndTree.scala b/src/main/scala/ap/proof/tree/AndTree.scala → ...rc/main/scala/ap/proof/tree/AndTree.scala
diff --git a/...roof/tree/IteratingProofTreeFactory.scala → ...roof/tree/IteratingProofTreeFactory.scala b/...roof/tree/IteratingProofTreeFactory.scala → ...roof/tree/IteratingProofTreeFactory.scala
diff --git a/src/main/scala/ap/proof/tree/ProofTree.scala → .../main/scala/ap/proof/tree/ProofTree.scala b/src/main/scala/ap/proof/tree/ProofTree.scala → .../main/scala/ap/proof/tree/ProofTree.scala
diff --git a/...cala/ap/proof/tree/ProofTreeFactory.scala → ...cala/ap/proof/tree/ProofTreeFactory.scala b/...cala/ap/proof/tree/ProofTreeFactory.scala → ...cala/ap/proof/tree/ProofTreeFactory.scala
diff --git a/...ala/ap/proof/tree/ProofTreeOneChild.scala → ...ala/ap/proof/tree/ProofTreeOneChild.scala b/...ala/ap/proof/tree/ProofTreeOneChild.scala → ...ala/ap/proof/tree/ProofTreeOneChild.scala
diff --git a/.../scala/ap/proof/tree/QuantifiedTree.scala → .../scala/ap/proof/tree/QuantifiedTree.scala b/.../scala/ap/proof/tree/QuantifiedTree.scala → .../scala/ap/proof/tree/QuantifiedTree.scala
diff --git a/...cala/ap/proof/tree/RandomDataSource.scala → ...cala/ap/proof/tree/RandomDataSource.scala b/...cala/ap/proof/tree/RandomDataSource.scala → ...cala/ap/proof/tree/RandomDataSource.scala
diff --git a/...p/proof/tree/SimpleProofTreeFactory.scala → ...p/proof/tree/SimpleProofTreeFactory.scala b/...p/proof/tree/SimpleProofTreeFactory.scala → ...p/proof/tree/SimpleProofTreeFactory.scala
diff --git a/.../scala/ap/proof/tree/StrengthenTree.scala → .../scala/ap/proof/tree/StrengthenTree.scala b/.../scala/ap/proof/tree/StrengthenTree.scala → .../scala/ap/proof/tree/StrengthenTree.scala
diff --git a/...n/scala/ap/proof/tree/TestProofTree.scala → ...n/scala/ap/proof/tree/TestProofTree.scala b/...n/scala/ap/proof/tree/TestProofTree.scala → ...n/scala/ap/proof/tree/TestProofTree.scala
diff --git a/...main/scala/ap/proof/tree/WeakenTree.scala → ...main/scala/ap/proof/tree/WeakenTree.scala b/...main/scala/ap/proof/tree/WeakenTree.scala → ...main/scala/ap/proof/tree/WeakenTree.scala
diff --git a/src/main/scala/ap/terfor/AliasStatus.scala → ...rc/main/scala/ap/terfor/AliasStatus.scala b/src/main/scala/ap/terfor/AliasStatus.scala → ...rc/main/scala/ap/terfor/AliasStatus.scala
diff --git a/...n/scala/ap/terfor/ComputationLogger.scala → ...n/scala/ap/terfor/ComputationLogger.scala b/...n/scala/ap/terfor/ComputationLogger.scala → ...n/scala/ap/terfor/ComputationLogger.scala
diff --git a/src/main/scala/ap/terfor/ConstantTerm.scala → ...c/main/scala/ap/terfor/ConstantTerm.scala b/src/main/scala/ap/terfor/ConstantTerm.scala → ...c/main/scala/ap/terfor/ConstantTerm.scala
diff --git a/src/main/scala/ap/terfor/Formula.scala → core/src/main/scala/ap/terfor/Formula.scala b/src/main/scala/ap/terfor/Formula.scala → core/src/main/scala/ap/terfor/Formula.scala
diff --git a/src/main/scala/ap/terfor/OneTerm.scala → core/src/main/scala/ap/terfor/OneTerm.scala b/src/main/scala/ap/terfor/OneTerm.scala → core/src/main/scala/ap/terfor/OneTerm.scala
diff --git a/src/main/scala/ap/terfor/Sorted.scala → core/src/main/scala/ap/terfor/Sorted.scala b/src/main/scala/ap/terfor/Sorted.scala → core/src/main/scala/ap/terfor/Sorted.scala
diff --git a/...ain/scala/ap/terfor/SortedWithOrder.scala → ...ain/scala/ap/terfor/SortedWithOrder.scala b/...ain/scala/ap/terfor/SortedWithOrder.scala → ...ain/scala/ap/terfor/SortedWithOrder.scala
diff --git a/src/main/scala/ap/terfor/TerFor.scala → core/src/main/scala/ap/terfor/TerFor.scala b/src/main/scala/ap/terfor/TerFor.scala → core/src/main/scala/ap/terfor/TerFor.scala
diff --git a/...n/scala/ap/terfor/TerForConvenience.scala → ...n/scala/ap/terfor/TerForConvenience.scala b/...n/scala/ap/terfor/TerForConvenience.scala → ...n/scala/ap/terfor/TerForConvenience.scala
diff --git a/src/main/scala/ap/terfor/Term.scala → core/src/main/scala/ap/terfor/Term.scala b/src/main/scala/ap/terfor/Term.scala → core/src/main/scala/ap/terfor/Term.scala
diff --git a/src/main/scala/ap/terfor/TermOrder.scala → .../src/main/scala/ap/terfor/TermOrder.scala b/src/main/scala/ap/terfor/TermOrder.scala → .../src/main/scala/ap/terfor/TermOrder.scala
diff --git a/src/main/scala/ap/terfor/VariableTerm.scala → ...c/main/scala/ap/terfor/VariableTerm.scala b/src/main/scala/ap/terfor/VariableTerm.scala → ...c/main/scala/ap/terfor/VariableTerm.scala
diff --git a/...scala/ap/terfor/arithconj/ArithConj.scala → ...scala/ap/terfor/arithconj/ArithConj.scala b/...scala/ap/terfor/arithconj/ArithConj.scala → ...scala/ap/terfor/arithconj/ArithConj.scala
diff --git a/...ala/ap/terfor/arithconj/ModelFinder.scala → ...ala/ap/terfor/arithconj/ModelFinder.scala b/...ala/ap/terfor/arithconj/ModelFinder.scala → ...ala/ap/terfor/arithconj/ModelFinder.scala
diff --git a/...la/ap/terfor/arithconj/ReduceWithAC.scala → ...la/ap/terfor/arithconj/ReduceWithAC.scala b/...la/ap/terfor/arithconj/ReduceWithAC.scala → ...la/ap/terfor/arithconj/ReduceWithAC.scala
diff --git a/...for/conjunctions/ConjunctEliminator.scala → ...for/conjunctions/ConjunctEliminator.scala b/...for/conjunctions/ConjunctEliminator.scala → ...for/conjunctions/ConjunctEliminator.scala
diff --git a/.../ap/terfor/conjunctions/Conjunction.scala → .../ap/terfor/conjunctions/Conjunction.scala b/.../ap/terfor/conjunctions/Conjunction.scala → .../ap/terfor/conjunctions/Conjunction.scala
diff --git a/...conjunctions/IterativeClauseMatcher.scala → ...conjunctions/IterativeClauseMatcher.scala b/...conjunctions/IterativeClauseMatcher.scala → ...conjunctions/IterativeClauseMatcher.scala
diff --git a/...terfor/conjunctions/LazyConjunction.scala → ...terfor/conjunctions/LazyConjunction.scala b/...terfor/conjunctions/LazyConjunction.scala → ...terfor/conjunctions/LazyConjunction.scala
diff --git a/...or/conjunctions/NegatedConjunctions.scala → ...or/conjunctions/NegatedConjunctions.scala b/...or/conjunctions/NegatedConjunctions.scala → ...or/conjunctions/NegatedConjunctions.scala
diff --git a/...a/ap/terfor/conjunctions/Quantifier.scala → ...a/ap/terfor/conjunctions/Quantifier.scala b/...a/ap/terfor/conjunctions/Quantifier.scala → ...a/ap/terfor/conjunctions/Quantifier.scala
diff --git a/.../conjunctions/ReduceWithConjunction.scala → .../conjunctions/ReduceWithConjunction.scala b/.../conjunctions/ReduceWithConjunction.scala → .../conjunctions/ReduceWithConjunction.scala
diff --git a/...p/terfor/conjunctions/ReducerPlugin.scala → ...p/terfor/conjunctions/ReducerPlugin.scala b/...p/terfor/conjunctions/ReducerPlugin.scala → ...p/terfor/conjunctions/ReducerPlugin.scala
diff --git a/...for/conjunctions/SubsumptionRemover.scala → ...for/conjunctions/SubsumptionRemover.scala b/...for/conjunctions/SubsumptionRemover.scala → ...for/conjunctions/SubsumptionRemover.scala
diff --git a/...la/ap/terfor/equations/ColumnSolver.scala → ...la/ap/terfor/equations/ColumnSolver.scala b/...la/ap/terfor/equations/ColumnSolver.scala → ...la/ap/terfor/equations/ColumnSolver.scala
diff --git a/...la/ap/terfor/equations/EquationConj.scala → ...la/ap/terfor/equations/EquationConj.scala b/...la/ap/terfor/equations/EquationConj.scala → ...la/ap/terfor/equations/EquationConj.scala
diff --git a/...ala/ap/terfor/equations/EquationSet.scala → ...ala/ap/terfor/equations/EquationSet.scala b/...ala/ap/terfor/equations/EquationSet.scala → ...ala/ap/terfor/equations/EquationSet.scala
diff --git a/...ap/terfor/equations/NegEquationConj.scala → ...ap/terfor/equations/NegEquationConj.scala b/...ap/terfor/equations/NegEquationConj.scala → ...ap/terfor/equations/NegEquationConj.scala
diff --git a/...a/ap/terfor/equations/ReduceWithEqs.scala → ...a/ap/terfor/equations/ReduceWithEqs.scala b/...a/ap/terfor/equations/ReduceWithEqs.scala → ...a/ap/terfor/equations/ReduceWithEqs.scala
diff --git a/...p/terfor/equations/ReduceWithNegEqs.scala → ...p/terfor/equations/ReduceWithNegEqs.scala b/...p/terfor/equations/ReduceWithNegEqs.scala → ...p/terfor/equations/ReduceWithNegEqs.scala
diff --git a/.../terfor/inequalities/FMInfsComputer.scala → .../terfor/inequalities/FMInfsComputer.scala b/.../terfor/inequalities/FMInfsComputer.scala → .../terfor/inequalities/FMInfsComputer.scala
diff --git a/...ala/ap/terfor/inequalities/InEqConj.scala → ...ala/ap/terfor/inequalities/InEqConj.scala b/...ala/ap/terfor/inequalities/InEqConj.scala → ...ala/ap/terfor/inequalities/InEqConj.scala
diff --git a/...ap/terfor/inequalities/IntervalProp.scala → ...ap/terfor/inequalities/IntervalProp.scala b/...ap/terfor/inequalities/IntervalProp.scala → ...ap/terfor/inequalities/IntervalProp.scala
diff --git a/...terfor/inequalities/ReduceWithInEqs.scala → ...terfor/inequalities/ReduceWithInEqs.scala b/...terfor/inequalities/ReduceWithInEqs.scala → ...terfor/inequalities/ReduceWithInEqs.scala
diff --git a/.../terfor/linearcombination/LCBlender.scala → .../terfor/linearcombination/LCBlender.scala b/.../terfor/linearcombination/LCBlender.scala → .../terfor/linearcombination/LCBlender.scala
diff --git a/...linearcombination/LinearCombination.scala → ...linearcombination/LinearCombination.scala b/...linearcombination/LinearCombination.scala → ...linearcombination/LinearCombination.scala
diff --git a/...r/linearcombination/ScalingIterator.scala → ...r/linearcombination/ScalingIterator.scala b/...r/linearcombination/ScalingIterator.scala → ...r/linearcombination/ScalingIterator.scala
diff --git a/src/main/scala/ap/terfor/preds/Atom.scala → ...src/main/scala/ap/terfor/preds/Atom.scala b/src/main/scala/ap/terfor/preds/Atom.scala → ...src/main/scala/ap/terfor/preds/Atom.scala
diff --git a/...main/scala/ap/terfor/preds/PredConj.scala → ...main/scala/ap/terfor/preds/PredConj.scala b/...main/scala/ap/terfor/preds/PredConj.scala → ...main/scala/ap/terfor/preds/PredConj.scala
diff --git a/...ain/scala/ap/terfor/preds/Predicate.scala → ...ain/scala/ap/terfor/preds/Predicate.scala b/...ain/scala/ap/terfor/preds/Predicate.scala → ...ain/scala/ap/terfor/preds/Predicate.scala
diff --git a/.../ap/terfor/preds/ReduceWithPredLits.scala → .../ap/terfor/preds/ReduceWithPredLits.scala b/.../ap/terfor/preds/ReduceWithPredLits.scala → .../ap/terfor/preds/ReduceWithPredLits.scala
diff --git a/.../terfor/substitutions/ComposeSubsts.scala → .../terfor/substitutions/ComposeSubsts.scala b/.../terfor/substitutions/ComposeSubsts.scala → .../terfor/substitutions/ComposeSubsts.scala
diff --git a/.../terfor/substitutions/ConstantSubst.scala → .../terfor/substitutions/ConstantSubst.scala b/.../terfor/substitutions/ConstantSubst.scala → .../terfor/substitutions/ConstantSubst.scala
diff --git a/.../terfor/substitutions/IdentitySubst.scala → .../terfor/substitutions/IdentitySubst.scala b/.../terfor/substitutions/IdentitySubst.scala → .../terfor/substitutions/IdentitySubst.scala
diff --git a/...r/substitutions/PseudoConstantSubst.scala → ...r/substitutions/PseudoConstantSubst.scala b/...r/substitutions/PseudoConstantSubst.scala → ...r/substitutions/PseudoConstantSubst.scala
diff --git a/...substitutions/PseudoDivSubstitution.scala → ...substitutions/PseudoDivSubstitution.scala b/...substitutions/PseudoDivSubstitution.scala → ...substitutions/PseudoDivSubstitution.scala
diff --git a/...or/substitutions/SimpleSubstitution.scala → ...or/substitutions/SimpleSubstitution.scala b/...or/substitutions/SimpleSubstitution.scala → ...or/substitutions/SimpleSubstitution.scala
diff --git a/...p/terfor/substitutions/Substitution.scala → ...p/terfor/substitutions/Substitution.scala b/...p/terfor/substitutions/Substitution.scala → ...p/terfor/substitutions/Substitution.scala
diff --git a/...or/substitutions/VariableShiftSubst.scala → ...or/substitutions/VariableShiftSubst.scala b/...or/substitutions/VariableShiftSubst.scala → ...or/substitutions/VariableShiftSubst.scala
diff --git a/.../terfor/substitutions/VariableSubst.scala → .../terfor/substitutions/VariableSubst.scala b/.../terfor/substitutions/VariableSubst.scala → .../terfor/substitutions/VariableSubst.scala
diff --git a/src/main/scala/ap/theories/ADT.scala → core/src/main/scala/ap/theories/ADT.scala b/src/main/scala/ap/theories/ADT.scala → core/src/main/scala/ap/theories/ADT.scala
@@ -42,8 +42,7 @@ import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction,
 import ap.terfor.{TermOrder, TerForConvenience, Formula, OneTerm, Term}
 import ap.terfor.preds.Atom
 import ap.terfor.substitutions.{VariableShiftSubst, VariableSubst}
-import ap.{SimpleAPI, PresburgerTools}
-import SimpleAPI.ProverStatus
+import ap.PresburgerTools
 import ap.types.{Sort, ProxySort, MonoSortedIFunction, SortedPredicate,
                  SortedConstantTerm, MonoSortedPredicate}
 import ap.proof.theoryPlugins.Plugin

diff --git a/.../ap/theories/BitShiftMultiplication.scala → .../ap/theories/BitShiftMultiplication.scala b/.../ap/theories/BitShiftMultiplication.scala → .../ap/theories/BitShiftMultiplication.scala
diff --git a/src/main/scala/ap/theories/DivZero.scala → .../src/main/scala/ap/theories/DivZero.scala b/src/main/scala/ap/theories/DivZero.scala → .../src/main/scala/ap/theories/DivZero.scala
diff --git a/...a/ap/theories/FunctionalConsistency.scala → ...a/ap/theories/FunctionalConsistency.scala b/...a/ap/theories/FunctionalConsistency.scala → ...a/ap/theories/FunctionalConsistency.scala
diff --git a/...in/scala/ap/theories/Incompleteness.scala → ...in/scala/ap/theories/Incompleteness.scala b/...in/scala/ap/theories/Incompleteness.scala → ...in/scala/ap/theories/Incompleteness.scala
diff --git a/src/main/scala/ap/theories/MulTheory.scala → ...rc/main/scala/ap/theories/MulTheory.scala b/src/main/scala/ap/theories/MulTheory.scala → ...rc/main/scala/ap/theories/MulTheory.scala
diff --git a/...ala/ap/theories/SaturationProcedure.scala → ...ala/ap/theories/SaturationProcedure.scala b/...ala/ap/theories/SaturationProcedure.scala → ...ala/ap/theories/SaturationProcedure.scala
diff --git a/src/main/scala/ap/theories/Theory.scala → core/src/main/scala/ap/theories/Theory.scala b/src/main/scala/ap/theories/Theory.scala → core/src/main/scala/ap/theories/Theory.scala
diff --git a/...ain/scala/ap/theories/TheoryBuilder.scala → ...ain/scala/ap/theories/TheoryBuilder.scala b/...ain/scala/ap/theories/TheoryBuilder.scala → ...ain/scala/ap/theories/TheoryBuilder.scala
diff --git a/...n/scala/ap/theories/TheoryCollector.scala → ...n/scala/ap/theories/TheoryCollector.scala b/...n/scala/ap/theories/TheoryCollector.scala → ...n/scala/ap/theories/TheoryCollector.scala
diff --git a/...in/scala/ap/theories/TheoryRegistry.scala → ...in/scala/ap/theories/TheoryRegistry.scala b/...in/scala/ap/theories/TheoryRegistry.scala → ...in/scala/ap/theories/TheoryRegistry.scala
diff --git a/...n/scala/ap/theories/ValueEnumerator.scala → ...n/scala/ap/theories/ValueEnumerator.scala b/...n/scala/ap/theories/ValueEnumerator.scala → ...n/scala/ap/theories/ValueEnumerator.scala
diff --git a/.../scala/ap/theories/arrays/CombArray.scala → .../scala/ap/theories/arrays/CombArray.scala b/.../scala/ap/theories/arrays/CombArray.scala → .../scala/ap/theories/arrays/CombArray.scala
diff --git a/...n/scala/ap/theories/arrays/ExtArray.scala → ...n/scala/ap/theories/arrays/ExtArray.scala b/...n/scala/ap/theories/arrays/ExtArray.scala → ...n/scala/ap/theories/arrays/ExtArray.scala
diff --git a/...cala/ap/theories/arrays/MinMaxArray.scala → ...cala/ap/theories/arrays/MinMaxArray.scala b/...cala/ap/theories/arrays/MinMaxArray.scala → ...cala/ap/theories/arrays/MinMaxArray.scala
diff --git a/.../scala/ap/theories/arrays/SetTheory.scala → .../scala/ap/theories/arrays/SetTheory.scala b/.../scala/ap/theories/arrays/SetTheory.scala → .../scala/ap/theories/arrays/SetTheory.scala
diff --git a/...cala/ap/theories/arrays/SimpleArray.scala → ...cala/ap/theories/arrays/SimpleArray.scala b/...cala/ap/theories/arrays/SimpleArray.scala → ...cala/ap/theories/arrays/SimpleArray.scala
diff --git a/...ries/bitvectors/ExtractArithEncoder.scala → ...ries/bitvectors/ExtractArithEncoder.scala b/...ries/bitvectors/ExtractArithEncoder.scala → ...ries/bitvectors/ExtractArithEncoder.scala
diff --git a/...theories/bitvectors/ModCastSplitter.scala → ...theories/bitvectors/ModCastSplitter.scala b/...theories/bitvectors/ModCastSplitter.scala → ...theories/bitvectors/ModCastSplitter.scala
diff --git a/...la/ap/theories/bitvectors/ModPlugin.scala → ...la/ap/theories/bitvectors/ModPlugin.scala b/...la/ap/theories/bitvectors/ModPlugin.scala → ...la/ap/theories/bitvectors/ModPlugin.scala
diff --git a/...heories/bitvectors/ModPostprocessor.scala → ...heories/bitvectors/ModPostprocessor.scala b/...heories/bitvectors/ModPostprocessor.scala → ...heories/bitvectors/ModPostprocessor.scala
diff --git a/...theories/bitvectors/ModPreprocessor.scala → ...theories/bitvectors/ModPreprocessor.scala b/...theories/bitvectors/ModPreprocessor.scala → ...theories/bitvectors/ModPreprocessor.scala
diff --git a/...a/ap/theories/bitvectors/ModReducer.scala → ...a/ap/theories/bitvectors/ModReducer.scala b/...a/ap/theories/bitvectors/ModReducer.scala → ...a/ap/theories/bitvectors/ModReducer.scala
diff --git a/...heories/bitvectors/ModuloArithmetic.scala → ...heories/bitvectors/ModuloArithmetic.scala b/...heories/bitvectors/ModuloArithmetic.scala → ...heories/bitvectors/ModuloArithmetic.scala
diff --git a/...n/scala/ap/theories/bitvectors/Ring.scala → ...n/scala/ap/theories/bitvectors/Ring.scala b/...n/scala/ap/theories/bitvectors/Ring.scala → ...n/scala/ap/theories/bitvectors/Ring.scala
diff --git a/...eories/bitvectors/ShiftCastSplitter.scala → ...eories/bitvectors/ShiftCastSplitter.scala b/...eories/bitvectors/ShiftCastSplitter.scala → ...eories/bitvectors/ShiftCastSplitter.scala
diff --git a/...n/scala/ap/theories/heaps/ArrayHeap.scala → ...n/scala/ap/theories/heaps/ArrayHeap.scala b/...n/scala/ap/theories/heaps/ArrayHeap.scala → ...n/scala/ap/theories/heaps/ArrayHeap.scala
diff --git a/src/main/scala/ap/theories/heaps/Heap.scala → ...c/main/scala/ap/theories/heaps/Heap.scala b/src/main/scala/ap/theories/heaps/Heap.scala → ...c/main/scala/ap/theories/heaps/Heap.scala
diff --git a/.../scala/ap/theories/heaps/NativeHeap.scala → .../scala/ap/theories/heaps/NativeHeap.scala b/.../scala/ap/theories/heaps/NativeHeap.scala → .../scala/ap/theories/heaps/NativeHeap.scala
diff --git a/...in/scala/ap/theories/nia/Buchberger.scala → ...in/scala/ap/theories/nia/Buchberger.scala b/...in/scala/ap/theories/nia/Buchberger.scala → ...in/scala/ap/theories/nia/Buchberger.scala