diff --git a/build.sbt b/build.sbt
index 91eb58569..6af27a839 100644
--- 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 b/core/src/main/scala/ap/PresburgerTools.scala
similarity index 100%
rename from src/main/scala/ap/PresburgerTools.scala
rename to core/src/main/scala/ap/PresburgerTools.scala
diff --git a/src/main/scala/ap/Prover.scala b/core/src/main/scala/ap/Prover.scala
similarity index 100%
rename from src/main/scala/ap/Prover.scala
rename to core/src/main/scala/ap/Prover.scala
diff --git a/src/main/scala/ap/Signature.scala b/core/src/main/scala/ap/Signature.scala
similarity index 100%
rename from src/main/scala/ap/Signature.scala
rename to core/src/main/scala/ap/Signature.scala
diff --git a/src/main/scala/ap/algebra/Group.scala b/core/src/main/scala/ap/algebra/Group.scala
similarity index 100%
rename from src/main/scala/ap/algebra/Group.scala
rename to core/src/main/scala/ap/algebra/Group.scala
diff --git a/src/main/scala/ap/algebra/Integers.scala b/core/src/main/scala/ap/algebra/Integers.scala
similarity index 100%
rename from src/main/scala/ap/algebra/Integers.scala
rename to core/src/main/scala/ap/algebra/Integers.scala
diff --git a/src/main/scala/ap/algebra/Ring.scala b/core/src/main/scala/ap/algebra/Ring.scala
similarity index 100%
rename from src/main/scala/ap/algebra/Ring.scala
rename to core/src/main/scala/ap/algebra/Ring.scala
diff --git a/src/main/scala/ap/algebra/package.scala b/core/src/main/scala/ap/algebra/package.scala
similarity index 100%
rename from src/main/scala/ap/algebra/package.scala
rename to core/src/main/scala/ap/algebra/package.scala
diff --git a/src/main/scala/ap/api/PartialModel.scala b/core/src/main/scala/ap/api/PartialModel.scala
similarity index 100%
rename from src/main/scala/ap/api/PartialModel.scala
rename to core/src/main/scala/ap/api/PartialModel.scala
diff --git a/src/main/scala/ap/basetypes/HeapCollector.scala b/core/src/main/scala/ap/basetypes/HeapCollector.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/HeapCollector.scala
rename to core/src/main/scala/ap/basetypes/HeapCollector.scala
diff --git a/src/main/scala/ap/basetypes/IdealInt.scala b/core/src/main/scala/ap/basetypes/IdealInt.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/IdealInt.scala
rename to core/src/main/scala/ap/basetypes/IdealInt.scala
diff --git a/src/main/scala/ap/basetypes/IdealRat.scala b/core/src/main/scala/ap/basetypes/IdealRat.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/IdealRat.scala
rename to core/src/main/scala/ap/basetypes/IdealRat.scala
diff --git a/src/main/scala/ap/basetypes/LeftistHeap.scala b/core/src/main/scala/ap/basetypes/LeftistHeap.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/LeftistHeap.scala
rename to core/src/main/scala/ap/basetypes/LeftistHeap.scala
diff --git a/src/main/scala/ap/basetypes/MultiSet.scala b/core/src/main/scala/ap/basetypes/MultiSet.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/MultiSet.scala
rename to core/src/main/scala/ap/basetypes/MultiSet.scala
diff --git a/src/main/scala/ap/basetypes/SetTrie.scala b/core/src/main/scala/ap/basetypes/SetTrie.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/SetTrie.scala
rename to core/src/main/scala/ap/basetypes/SetTrie.scala
diff --git a/src/main/scala/ap/basetypes/Tree.scala b/core/src/main/scala/ap/basetypes/Tree.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/Tree.scala
rename to core/src/main/scala/ap/basetypes/Tree.scala
diff --git a/src/main/scala/ap/basetypes/UnionFind.scala b/core/src/main/scala/ap/basetypes/UnionFind.scala
similarity index 100%
rename from src/main/scala/ap/basetypes/UnionFind.scala
rename to core/src/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
new file mode 100644
index 000000000..3c1679f6c
--- /dev/null
+++ 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/src/main/scala/ap/interpolants/BenchUtils.scala b/core/src/main/scala/ap/interpolants/BenchUtils.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/BenchUtils.scala
rename to core/src/main/scala/ap/interpolants/BenchUtils.scala
diff --git a/src/main/scala/ap/interpolants/InterpolantSimplifier.scala b/core/src/main/scala/ap/interpolants/InterpolantSimplifier.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/InterpolantSimplifier.scala
rename to core/src/main/scala/ap/interpolants/InterpolantSimplifier.scala
diff --git a/src/main/scala/ap/interpolants/InterpolationContext.scala b/core/src/main/scala/ap/interpolants/InterpolationContext.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/InterpolationContext.scala
rename to core/src/main/scala/ap/interpolants/InterpolationContext.scala
diff --git a/src/main/scala/ap/interpolants/Interpolator.scala b/core/src/main/scala/ap/interpolants/Interpolator.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/Interpolator.scala
rename to core/src/main/scala/ap/interpolants/Interpolator.scala
diff --git a/src/main/scala/ap/interpolants/InterpolatorQE.scala b/core/src/main/scala/ap/interpolants/InterpolatorQE.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/InterpolatorQE.scala
rename to core/src/main/scala/ap/interpolants/InterpolatorQE.scala
diff --git a/src/main/scala/ap/interpolants/PartialInterpolant.scala b/core/src/main/scala/ap/interpolants/PartialInterpolant.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/PartialInterpolant.scala
rename to core/src/main/scala/ap/interpolants/PartialInterpolant.scala
diff --git a/src/main/scala/ap/interpolants/ProofSimplifier.scala b/core/src/main/scala/ap/interpolants/ProofSimplifier.scala
similarity index 100%
rename from src/main/scala/ap/interpolants/ProofSimplifier.scala
rename to core/src/main/scala/ap/interpolants/ProofSimplifier.scala
diff --git a/src/main/scala/ap/parameters/Param.scala b/core/src/main/scala/ap/parameters/Param.scala
similarity index 100%
rename from src/main/scala/ap/parameters/Param.scala
rename to core/src/main/scala/ap/parameters/Param.scala
diff --git a/src/main/scala/ap/parameters/Settings.scala b/core/src/main/scala/ap/parameters/Settings.scala
similarity index 100%
rename from src/main/scala/ap/parameters/Settings.scala
rename to core/src/main/scala/ap/parameters/Settings.scala
diff --git a/src/main/scala/ap/parser/BooleanCompactifier.scala b/core/src/main/scala/ap/parser/BooleanCompactifier.scala
similarity index 100%
rename from src/main/scala/ap/parser/BooleanCompactifier.scala
rename to core/src/main/scala/ap/parser/BooleanCompactifier.scala
diff --git a/src/main/scala/ap/parser/CSIsatLineariser.scala b/core/src/main/scala/ap/parser/CSIsatLineariser.scala
similarity index 100%
rename from src/main/scala/ap/parser/CSIsatLineariser.scala
rename to core/src/main/scala/ap/parser/CSIsatLineariser.scala
diff --git a/src/main/scala/ap/parser/Environment.scala b/core/src/main/scala/ap/parser/Environment.scala
similarity index 100%
rename from src/main/scala/ap/parser/Environment.scala
rename to core/src/main/scala/ap/parser/Environment.scala
diff --git a/src/main/scala/ap/parser/EquivExpander.scala b/core/src/main/scala/ap/parser/EquivExpander.scala
similarity index 100%
rename from src/main/scala/ap/parser/EquivExpander.scala
rename to core/src/main/scala/ap/parser/EquivExpander.scala
diff --git a/src/main/scala/ap/parser/EquivInliner.scala b/core/src/main/scala/ap/parser/EquivInliner.scala
similarity index 100%
rename from src/main/scala/ap/parser/EquivInliner.scala
rename to core/src/main/scala/ap/parser/EquivInliner.scala
diff --git a/src/main/scala/ap/parser/ExMaxiscoper.scala b/core/src/main/scala/ap/parser/ExMaxiscoper.scala
similarity index 100%
rename from src/main/scala/ap/parser/ExMaxiscoper.scala
rename to core/src/main/scala/ap/parser/ExMaxiscoper.scala
diff --git a/src/main/scala/ap/parser/FunctionEncoder.scala b/core/src/main/scala/ap/parser/FunctionEncoder.scala
similarity index 100%
rename from src/main/scala/ap/parser/FunctionEncoder.scala
rename to core/src/main/scala/ap/parser/FunctionEncoder.scala
diff --git a/src/main/scala/ap/parser/FunctionPreprocessing.scala b/core/src/main/scala/ap/parser/FunctionPreprocessing.scala
similarity index 100%
rename from src/main/scala/ap/parser/FunctionPreprocessing.scala
rename to core/src/main/scala/ap/parser/FunctionPreprocessing.scala
diff --git a/src/main/scala/ap/parser/IExpression.scala b/core/src/main/scala/ap/parser/IExpression.scala
similarity index 100%
rename from src/main/scala/ap/parser/IExpression.scala
rename to core/src/main/scala/ap/parser/IExpression.scala
diff --git a/src/main/scala/ap/parser/IFormula.scala b/core/src/main/scala/ap/parser/IFormula.scala
similarity index 100%
rename from src/main/scala/ap/parser/IFormula.scala
rename to core/src/main/scala/ap/parser/IFormula.scala
diff --git a/src/main/scala/ap/parser/ITerm.scala b/core/src/main/scala/ap/parser/ITerm.scala
similarity index 100%
rename from src/main/scala/ap/parser/ITerm.scala
rename to core/src/main/scala/ap/parser/ITerm.scala
diff --git a/src/main/scala/ap/parser/ImplicationCompressor.scala b/core/src/main/scala/ap/parser/ImplicationCompressor.scala
similarity index 100%
rename from src/main/scala/ap/parser/ImplicationCompressor.scala
rename to core/src/main/scala/ap/parser/ImplicationCompressor.scala
diff --git a/src/main/scala/ap/parser/InputAbsy2Internal.scala b/core/src/main/scala/ap/parser/InputAbsy2Internal.scala
similarity index 100%
rename from src/main/scala/ap/parser/InputAbsy2Internal.scala
rename to core/src/main/scala/ap/parser/InputAbsy2Internal.scala
diff --git a/src/main/scala/ap/parser/InputAbsyVisitor.scala b/core/src/main/scala/ap/parser/InputAbsyVisitor.scala
similarity index 100%
rename from src/main/scala/ap/parser/InputAbsyVisitor.scala
rename to core/src/main/scala/ap/parser/InputAbsyVisitor.scala
diff --git a/src/main/scala/ap/parser/Internal2InputAbsy.scala b/core/src/main/scala/ap/parser/Internal2InputAbsy.scala
similarity index 100%
rename from src/main/scala/ap/parser/Internal2InputAbsy.scala
rename to core/src/main/scala/ap/parser/Internal2InputAbsy.scala
diff --git a/src/main/scala/ap/parser/KBO.scala b/core/src/main/scala/ap/parser/KBO.scala
similarity index 100%
rename from src/main/scala/ap/parser/KBO.scala
rename to core/src/main/scala/ap/parser/KBO.scala
diff --git a/src/main/scala/ap/parser/Parser2InputAbsy.scala b/core/src/main/scala/ap/parser/Parser2InputAbsy.scala
similarity index 100%
rename from src/main/scala/ap/parser/Parser2InputAbsy.scala
rename to core/src/main/scala/ap/parser/Parser2InputAbsy.scala
diff --git a/src/main/scala/ap/parser/PartExtractor.scala b/core/src/main/scala/ap/parser/PartExtractor.scala
similarity index 100%
rename from src/main/scala/ap/parser/PartExtractor.scala
rename to core/src/main/scala/ap/parser/PartExtractor.scala
diff --git a/src/main/scala/ap/parser/PartialEvaluator.scala b/core/src/main/scala/ap/parser/PartialEvaluator.scala
similarity index 100%
rename from src/main/scala/ap/parser/PartialEvaluator.scala
rename to core/src/main/scala/ap/parser/PartialEvaluator.scala
diff --git a/src/main/scala/ap/parser/Postprocessing.scala b/core/src/main/scala/ap/parser/Postprocessing.scala
similarity index 100%
rename from src/main/scala/ap/parser/Postprocessing.scala
rename to core/src/main/scala/ap/parser/Postprocessing.scala
diff --git a/src/main/scala/ap/parser/Preprocessing.scala b/core/src/main/scala/ap/parser/Preprocessing.scala
similarity index 100%
rename from src/main/scala/ap/parser/Preprocessing.scala
rename to core/src/main/scala/ap/parser/Preprocessing.scala
diff --git a/src/main/scala/ap/parser/Rewriter.scala b/core/src/main/scala/ap/parser/Rewriter.scala
similarity index 100%
rename from src/main/scala/ap/parser/Rewriter.scala
rename to core/src/main/scala/ap/parser/Rewriter.scala
diff --git a/src/main/scala/ap/parser/SMTLineariser.scala b/core/src/main/scala/ap/parser/SMTLineariser.scala
similarity index 98%
rename from src/main/scala/ap/parser/SMTLineariser.scala
rename to core/src/main/scala/ap/parser/SMTLineariser.scala
index b15f4a1d0..defd893fa 100644
--- a/src/main/scala/ap/parser/SMTLineariser.scala
+++ b/core/src/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/src/main/scala/ap/parser/SMTParseableTheory.scala b/core/src/main/scala/ap/parser/SMTParseableTheory.scala
similarity index 95%
rename from src/main/scala/ap/parser/SMTParseableTheory.scala
rename to core/src/main/scala/ap/parser/SMTParseableTheory.scala
index b268eaa21..31d8c8027 100644
--- a/src/main/scala/ap/parser/SMTParseableTheory.scala
+++ b/core/src/main/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,10 +88,13 @@ 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
@@ -100,7 +102,7 @@ trait SMTParseableTheory {
    * 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
new file mode 100644
index 000000000..ba3519be4
--- /dev/null
+++ 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 b/core/src/main/scala/ap/parser/SMTTypes.scala
similarity index 96%
rename from src/main/scala/ap/parser/SMTTypes.scala
rename to core/src/main/scala/ap/parser/SMTTypes.scala
index c315997fe..17dc2d3c0 100644
--- a/src/main/scala/ap/parser/SMTTypes.scala
+++ b/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/src/main/scala/ap/parser/SimpleClausifier.scala b/core/src/main/scala/ap/parser/SimpleClausifier.scala
similarity index 100%
rename from src/main/scala/ap/parser/SimpleClausifier.scala
rename to core/src/main/scala/ap/parser/SimpleClausifier.scala
diff --git a/src/main/scala/ap/parser/SimpleMiniscoper.scala b/core/src/main/scala/ap/parser/SimpleMiniscoper.scala
similarity index 100%
rename from src/main/scala/ap/parser/SimpleMiniscoper.scala
rename to core/src/main/scala/ap/parser/SimpleMiniscoper.scala
diff --git a/src/main/scala/ap/parser/Simplifier.scala b/core/src/main/scala/ap/parser/Simplifier.scala
similarity index 100%
rename from src/main/scala/ap/parser/Simplifier.scala
rename to core/src/main/scala/ap/parser/Simplifier.scala
diff --git a/src/main/scala/ap/parser/TPTPLineariser.scala b/core/src/main/scala/ap/parser/TPTPLineariser.scala
similarity index 100%
rename from src/main/scala/ap/parser/TPTPLineariser.scala
rename to core/src/main/scala/ap/parser/TPTPLineariser.scala
diff --git a/src/main/scala/ap/parser/TriggerGenerator.scala b/core/src/main/scala/ap/parser/TriggerGenerator.scala
similarity index 100%
rename from src/main/scala/ap/parser/TriggerGenerator.scala
rename to core/src/main/scala/ap/parser/TriggerGenerator.scala
diff --git a/src/main/scala/ap/proof/BindingContext.scala b/core/src/main/scala/ap/proof/BindingContext.scala
similarity index 100%
rename from src/main/scala/ap/proof/BindingContext.scala
rename to core/src/main/scala/ap/proof/BindingContext.scala
diff --git a/src/main/scala/ap/proof/ConstantFreedom.scala b/core/src/main/scala/ap/proof/ConstantFreedom.scala
similarity index 100%
rename from src/main/scala/ap/proof/ConstantFreedom.scala
rename to core/src/main/scala/ap/proof/ConstantFreedom.scala
diff --git a/src/main/scala/ap/proof/ConstraintSimplifier.scala b/core/src/main/scala/ap/proof/ConstraintSimplifier.scala
similarity index 95%
rename from src/main/scala/ap/proof/ConstraintSimplifier.scala
rename to core/src/main/scala/ap/proof/ConstraintSimplifier.scala
index a4abf37c2..def0af454 100644
--- a/src/main/scala/ap/proof/ConstraintSimplifier.scala
+++ b/core/src/main/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/src/main/scala/ap/proof/ExhaustiveProver.scala b/core/src/main/scala/ap/proof/ExhaustiveProver.scala
similarity index 100%
rename from src/main/scala/ap/proof/ExhaustiveProver.scala
rename to core/src/main/scala/ap/proof/ExhaustiveProver.scala
diff --git a/src/main/scala/ap/proof/ModelSearchProver.scala b/core/src/main/scala/ap/proof/ModelSearchProver.scala
similarity index 97%
rename from src/main/scala/ap/proof/ModelSearchProver.scala
rename to core/src/main/scala/ap/proof/ModelSearchProver.scala
index ee8ce49bc..0c12cc15a 100644
--- a/src/main/scala/ap/proof/ModelSearchProver.scala
+++ b/core/src/main/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/src/main/scala/ap/proof/QuantifierElimProver.scala b/core/src/main/scala/ap/proof/QuantifierElimProver.scala
similarity index 100%
rename from src/main/scala/ap/proof/QuantifierElimProver.scala
rename to core/src/main/scala/ap/proof/QuantifierElimProver.scala
diff --git a/src/main/scala/ap/proof/Vocabulary.scala b/core/src/main/scala/ap/proof/Vocabulary.scala
similarity index 100%
rename from src/main/scala/ap/proof/Vocabulary.scala
rename to core/src/main/scala/ap/proof/Vocabulary.scala
diff --git a/src/main/scala/ap/proof/certificates/BinaryCertificate.scala b/core/src/main/scala/ap/proof/certificates/BinaryCertificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/BinaryCertificate.scala
rename to core/src/main/scala/ap/proof/certificates/BinaryCertificate.scala
diff --git a/src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala b/core/src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala
rename to core/src/main/scala/ap/proof/certificates/BranchInferenceCollection.scala
diff --git a/src/main/scala/ap/proof/certificates/CertFormula.scala b/core/src/main/scala/ap/proof/certificates/CertFormula.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/CertFormula.scala
rename to core/src/main/scala/ap/proof/certificates/CertFormula.scala
diff --git a/src/main/scala/ap/proof/certificates/Certificate.scala b/core/src/main/scala/ap/proof/certificates/Certificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/Certificate.scala
rename to core/src/main/scala/ap/proof/certificates/Certificate.scala
diff --git a/src/main/scala/ap/proof/certificates/CertificateOneChild.scala b/core/src/main/scala/ap/proof/certificates/CertificateOneChild.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/CertificateOneChild.scala
rename to core/src/main/scala/ap/proof/certificates/CertificateOneChild.scala
diff --git a/src/main/scala/ap/proof/certificates/CloseCertificate.scala b/core/src/main/scala/ap/proof/certificates/CloseCertificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/CloseCertificate.scala
rename to core/src/main/scala/ap/proof/certificates/CloseCertificate.scala
diff --git a/src/main/scala/ap/proof/certificates/DagCertificateConverter.scala b/core/src/main/scala/ap/proof/certificates/DagCertificateConverter.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/DagCertificateConverter.scala
rename to core/src/main/scala/ap/proof/certificates/DagCertificateConverter.scala
diff --git a/src/main/scala/ap/proof/certificates/DotLineariser.scala b/core/src/main/scala/ap/proof/certificates/DotLineariser.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/DotLineariser.scala
rename to core/src/main/scala/ap/proof/certificates/DotLineariser.scala
diff --git a/src/main/scala/ap/proof/certificates/LemmaBase.scala b/core/src/main/scala/ap/proof/certificates/LemmaBase.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/LemmaBase.scala
rename to core/src/main/scala/ap/proof/certificates/LemmaBase.scala
diff --git a/src/main/scala/ap/proof/certificates/OmegaCertificate.scala b/core/src/main/scala/ap/proof/certificates/OmegaCertificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/OmegaCertificate.scala
rename to core/src/main/scala/ap/proof/certificates/OmegaCertificate.scala
diff --git a/src/main/scala/ap/proof/certificates/PropCertificate.scala b/core/src/main/scala/ap/proof/certificates/PropCertificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/PropCertificate.scala
rename to core/src/main/scala/ap/proof/certificates/PropCertificate.scala
diff --git a/src/main/scala/ap/proof/certificates/SplitEqCertificate.scala b/core/src/main/scala/ap/proof/certificates/SplitEqCertificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/SplitEqCertificate.scala
rename to core/src/main/scala/ap/proof/certificates/SplitEqCertificate.scala
diff --git a/src/main/scala/ap/proof/certificates/StrengthenCertificate.scala b/core/src/main/scala/ap/proof/certificates/StrengthenCertificate.scala
similarity index 100%
rename from src/main/scala/ap/proof/certificates/StrengthenCertificate.scala
rename to core/src/main/scala/ap/proof/certificates/StrengthenCertificate.scala
diff --git a/src/main/scala/ap/proof/goal/AddFactsTask.scala b/core/src/main/scala/ap/proof/goal/AddFactsTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/AddFactsTask.scala
rename to core/src/main/scala/ap/proof/goal/AddFactsTask.scala
diff --git a/src/main/scala/ap/proof/goal/AliasAnalyser.scala b/core/src/main/scala/ap/proof/goal/AliasAnalyser.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/AliasAnalyser.scala
rename to core/src/main/scala/ap/proof/goal/AliasAnalyser.scala
diff --git a/src/main/scala/ap/proof/goal/AllQuantifierTask.scala b/core/src/main/scala/ap/proof/goal/AllQuantifierTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/AllQuantifierTask.scala
rename to core/src/main/scala/ap/proof/goal/AllQuantifierTask.scala
diff --git a/src/main/scala/ap/proof/goal/BetaFormulaTask.scala b/core/src/main/scala/ap/proof/goal/BetaFormulaTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/BetaFormulaTask.scala
rename to core/src/main/scala/ap/proof/goal/BetaFormulaTask.scala
diff --git a/src/main/scala/ap/proof/goal/BlockedFormulaTask.scala b/core/src/main/scala/ap/proof/goal/BlockedFormulaTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/BlockedFormulaTask.scala
rename to core/src/main/scala/ap/proof/goal/BlockedFormulaTask.scala
diff --git a/src/main/scala/ap/proof/goal/BoundStrengthenTask.scala b/core/src/main/scala/ap/proof/goal/BoundStrengthenTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/BoundStrengthenTask.scala
rename to core/src/main/scala/ap/proof/goal/BoundStrengthenTask.scala
diff --git a/src/main/scala/ap/proof/goal/CompoundFormulas.scala b/core/src/main/scala/ap/proof/goal/CompoundFormulas.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/CompoundFormulas.scala
rename to core/src/main/scala/ap/proof/goal/CompoundFormulas.scala
diff --git a/src/main/scala/ap/proof/goal/DivisibilityTask.scala b/core/src/main/scala/ap/proof/goal/DivisibilityTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/DivisibilityTask.scala
rename to core/src/main/scala/ap/proof/goal/DivisibilityTask.scala
diff --git a/src/main/scala/ap/proof/goal/EagerTask.scala b/core/src/main/scala/ap/proof/goal/EagerTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/EagerTask.scala
rename to core/src/main/scala/ap/proof/goal/EagerTask.scala
diff --git a/src/main/scala/ap/proof/goal/EagerTaskManager.scala b/core/src/main/scala/ap/proof/goal/EagerTaskManager.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/EagerTaskManager.scala
rename to core/src/main/scala/ap/proof/goal/EagerTaskManager.scala
diff --git a/src/main/scala/ap/proof/goal/EliminateFactsTask.scala b/core/src/main/scala/ap/proof/goal/EliminateFactsTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/EliminateFactsTask.scala
rename to core/src/main/scala/ap/proof/goal/EliminateFactsTask.scala
diff --git a/src/main/scala/ap/proof/goal/ExQuantifierTask.scala b/core/src/main/scala/ap/proof/goal/ExQuantifierTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/ExQuantifierTask.scala
rename to core/src/main/scala/ap/proof/goal/ExQuantifierTask.scala
diff --git a/src/main/scala/ap/proof/goal/FactsNormalisationTask.scala b/core/src/main/scala/ap/proof/goal/FactsNormalisationTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/FactsNormalisationTask.scala
rename to core/src/main/scala/ap/proof/goal/FactsNormalisationTask.scala
diff --git a/src/main/scala/ap/proof/goal/FormulaTask.scala b/core/src/main/scala/ap/proof/goal/FormulaTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/FormulaTask.scala
rename to core/src/main/scala/ap/proof/goal/FormulaTask.scala
diff --git a/src/main/scala/ap/proof/goal/Goal.scala b/core/src/main/scala/ap/proof/goal/Goal.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/Goal.scala
rename to core/src/main/scala/ap/proof/goal/Goal.scala
diff --git a/src/main/scala/ap/proof/goal/MatchTasks.scala b/core/src/main/scala/ap/proof/goal/MatchTasks.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/MatchTasks.scala
rename to core/src/main/scala/ap/proof/goal/MatchTasks.scala
diff --git a/src/main/scala/ap/proof/goal/NegLitClauseTask.scala b/core/src/main/scala/ap/proof/goal/NegLitClauseTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/NegLitClauseTask.scala
rename to core/src/main/scala/ap/proof/goal/NegLitClauseTask.scala
diff --git a/src/main/scala/ap/proof/goal/OmegaTask.scala b/core/src/main/scala/ap/proof/goal/OmegaTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/OmegaTask.scala
rename to core/src/main/scala/ap/proof/goal/OmegaTask.scala
diff --git a/src/main/scala/ap/proof/goal/PrioritisedTask.scala b/core/src/main/scala/ap/proof/goal/PrioritisedTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/PrioritisedTask.scala
rename to core/src/main/scala/ap/proof/goal/PrioritisedTask.scala
diff --git a/src/main/scala/ap/proof/goal/QuantifierTask.scala b/core/src/main/scala/ap/proof/goal/QuantifierTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/QuantifierTask.scala
rename to core/src/main/scala/ap/proof/goal/QuantifierTask.scala
diff --git a/src/main/scala/ap/proof/goal/SymbolWeigths.scala b/core/src/main/scala/ap/proof/goal/SymbolWeigths.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/SymbolWeigths.scala
rename to core/src/main/scala/ap/proof/goal/SymbolWeigths.scala
diff --git a/src/main/scala/ap/proof/goal/Task.scala b/core/src/main/scala/ap/proof/goal/Task.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/Task.scala
rename to core/src/main/scala/ap/proof/goal/Task.scala
diff --git a/src/main/scala/ap/proof/goal/TaskAggregator.scala b/core/src/main/scala/ap/proof/goal/TaskAggregator.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/TaskAggregator.scala
rename to core/src/main/scala/ap/proof/goal/TaskAggregator.scala
diff --git a/src/main/scala/ap/proof/goal/TaskManager.scala b/core/src/main/scala/ap/proof/goal/TaskManager.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/TaskManager.scala
rename to core/src/main/scala/ap/proof/goal/TaskManager.scala
diff --git a/src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala b/core/src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala
rename to core/src/main/scala/ap/proof/goal/UpdateConstantFreedomTask.scala
diff --git a/src/main/scala/ap/proof/goal/UpdateTasksTask.scala b/core/src/main/scala/ap/proof/goal/UpdateTasksTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/UpdateTasksTask.scala
rename to core/src/main/scala/ap/proof/goal/UpdateTasksTask.scala
diff --git a/src/main/scala/ap/proof/goal/WrappedFormulaTask.scala b/core/src/main/scala/ap/proof/goal/WrappedFormulaTask.scala
similarity index 100%
rename from src/main/scala/ap/proof/goal/WrappedFormulaTask.scala
rename to core/src/main/scala/ap/proof/goal/WrappedFormulaTask.scala
diff --git a/src/main/scala/ap/proof/theoryPlugins/Plugin.scala b/core/src/main/scala/ap/proof/theoryPlugins/Plugin.scala
similarity index 100%
rename from src/main/scala/ap/proof/theoryPlugins/Plugin.scala
rename to core/src/main/scala/ap/proof/theoryPlugins/Plugin.scala
diff --git a/src/main/scala/ap/proof/tree/AndTree.scala b/core/src/main/scala/ap/proof/tree/AndTree.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/AndTree.scala
rename to core/src/main/scala/ap/proof/tree/AndTree.scala
diff --git a/src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala b/core/src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala
rename to core/src/main/scala/ap/proof/tree/IteratingProofTreeFactory.scala
diff --git a/src/main/scala/ap/proof/tree/ProofTree.scala b/core/src/main/scala/ap/proof/tree/ProofTree.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/ProofTree.scala
rename to core/src/main/scala/ap/proof/tree/ProofTree.scala
diff --git a/src/main/scala/ap/proof/tree/ProofTreeFactory.scala b/core/src/main/scala/ap/proof/tree/ProofTreeFactory.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/ProofTreeFactory.scala
rename to core/src/main/scala/ap/proof/tree/ProofTreeFactory.scala
diff --git a/src/main/scala/ap/proof/tree/ProofTreeOneChild.scala b/core/src/main/scala/ap/proof/tree/ProofTreeOneChild.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/ProofTreeOneChild.scala
rename to core/src/main/scala/ap/proof/tree/ProofTreeOneChild.scala
diff --git a/src/main/scala/ap/proof/tree/QuantifiedTree.scala b/core/src/main/scala/ap/proof/tree/QuantifiedTree.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/QuantifiedTree.scala
rename to core/src/main/scala/ap/proof/tree/QuantifiedTree.scala
diff --git a/src/main/scala/ap/proof/tree/RandomDataSource.scala b/core/src/main/scala/ap/proof/tree/RandomDataSource.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/RandomDataSource.scala
rename to core/src/main/scala/ap/proof/tree/RandomDataSource.scala
diff --git a/src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala b/core/src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala
rename to core/src/main/scala/ap/proof/tree/SimpleProofTreeFactory.scala
diff --git a/src/main/scala/ap/proof/tree/StrengthenTree.scala b/core/src/main/scala/ap/proof/tree/StrengthenTree.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/StrengthenTree.scala
rename to core/src/main/scala/ap/proof/tree/StrengthenTree.scala
diff --git a/src/main/scala/ap/proof/tree/TestProofTree.scala b/core/src/main/scala/ap/proof/tree/TestProofTree.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/TestProofTree.scala
rename to core/src/main/scala/ap/proof/tree/TestProofTree.scala
diff --git a/src/main/scala/ap/proof/tree/WeakenTree.scala b/core/src/main/scala/ap/proof/tree/WeakenTree.scala
similarity index 100%
rename from src/main/scala/ap/proof/tree/WeakenTree.scala
rename to core/src/main/scala/ap/proof/tree/WeakenTree.scala
diff --git a/src/main/scala/ap/terfor/AliasStatus.scala b/core/src/main/scala/ap/terfor/AliasStatus.scala
similarity index 100%
rename from src/main/scala/ap/terfor/AliasStatus.scala
rename to core/src/main/scala/ap/terfor/AliasStatus.scala
diff --git a/src/main/scala/ap/terfor/ComputationLogger.scala b/core/src/main/scala/ap/terfor/ComputationLogger.scala
similarity index 100%
rename from src/main/scala/ap/terfor/ComputationLogger.scala
rename to core/src/main/scala/ap/terfor/ComputationLogger.scala
diff --git a/src/main/scala/ap/terfor/ConstantTerm.scala b/core/src/main/scala/ap/terfor/ConstantTerm.scala
similarity index 100%
rename from src/main/scala/ap/terfor/ConstantTerm.scala
rename to core/src/main/scala/ap/terfor/ConstantTerm.scala
diff --git a/src/main/scala/ap/terfor/Formula.scala b/core/src/main/scala/ap/terfor/Formula.scala
similarity index 100%
rename from src/main/scala/ap/terfor/Formula.scala
rename to core/src/main/scala/ap/terfor/Formula.scala
diff --git a/src/main/scala/ap/terfor/OneTerm.scala b/core/src/main/scala/ap/terfor/OneTerm.scala
similarity index 100%
rename from src/main/scala/ap/terfor/OneTerm.scala
rename to core/src/main/scala/ap/terfor/OneTerm.scala
diff --git a/src/main/scala/ap/terfor/Sorted.scala b/core/src/main/scala/ap/terfor/Sorted.scala
similarity index 100%
rename from src/main/scala/ap/terfor/Sorted.scala
rename to core/src/main/scala/ap/terfor/Sorted.scala
diff --git a/src/main/scala/ap/terfor/SortedWithOrder.scala b/core/src/main/scala/ap/terfor/SortedWithOrder.scala
similarity index 100%
rename from src/main/scala/ap/terfor/SortedWithOrder.scala
rename to core/src/main/scala/ap/terfor/SortedWithOrder.scala
diff --git a/src/main/scala/ap/terfor/TerFor.scala b/core/src/main/scala/ap/terfor/TerFor.scala
similarity index 100%
rename from src/main/scala/ap/terfor/TerFor.scala
rename to core/src/main/scala/ap/terfor/TerFor.scala
diff --git a/src/main/scala/ap/terfor/TerForConvenience.scala b/core/src/main/scala/ap/terfor/TerForConvenience.scala
similarity index 100%
rename from src/main/scala/ap/terfor/TerForConvenience.scala
rename to core/src/main/scala/ap/terfor/TerForConvenience.scala
diff --git a/src/main/scala/ap/terfor/Term.scala b/core/src/main/scala/ap/terfor/Term.scala
similarity index 100%
rename from src/main/scala/ap/terfor/Term.scala
rename to core/src/main/scala/ap/terfor/Term.scala
diff --git a/src/main/scala/ap/terfor/TermOrder.scala b/core/src/main/scala/ap/terfor/TermOrder.scala
similarity index 100%
rename from src/main/scala/ap/terfor/TermOrder.scala
rename to core/src/main/scala/ap/terfor/TermOrder.scala
diff --git a/src/main/scala/ap/terfor/VariableTerm.scala b/core/src/main/scala/ap/terfor/VariableTerm.scala
similarity index 100%
rename from src/main/scala/ap/terfor/VariableTerm.scala
rename to core/src/main/scala/ap/terfor/VariableTerm.scala
diff --git a/src/main/scala/ap/terfor/arithconj/ArithConj.scala b/core/src/main/scala/ap/terfor/arithconj/ArithConj.scala
similarity index 100%
rename from src/main/scala/ap/terfor/arithconj/ArithConj.scala
rename to core/src/main/scala/ap/terfor/arithconj/ArithConj.scala
diff --git a/src/main/scala/ap/terfor/arithconj/ModelFinder.scala b/core/src/main/scala/ap/terfor/arithconj/ModelFinder.scala
similarity index 100%
rename from src/main/scala/ap/terfor/arithconj/ModelFinder.scala
rename to core/src/main/scala/ap/terfor/arithconj/ModelFinder.scala
diff --git a/src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala b/core/src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala
similarity index 100%
rename from src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala
rename to core/src/main/scala/ap/terfor/arithconj/ReduceWithAC.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala b/core/src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala
rename to core/src/main/scala/ap/terfor/conjunctions/ConjunctEliminator.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/Conjunction.scala b/core/src/main/scala/ap/terfor/conjunctions/Conjunction.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/Conjunction.scala
rename to core/src/main/scala/ap/terfor/conjunctions/Conjunction.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala b/core/src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala
rename to core/src/main/scala/ap/terfor/conjunctions/IterativeClauseMatcher.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala b/core/src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala
rename to core/src/main/scala/ap/terfor/conjunctions/LazyConjunction.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala b/core/src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala
rename to core/src/main/scala/ap/terfor/conjunctions/NegatedConjunctions.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/Quantifier.scala b/core/src/main/scala/ap/terfor/conjunctions/Quantifier.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/Quantifier.scala
rename to core/src/main/scala/ap/terfor/conjunctions/Quantifier.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala b/core/src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala
rename to core/src/main/scala/ap/terfor/conjunctions/ReduceWithConjunction.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala b/core/src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala
rename to core/src/main/scala/ap/terfor/conjunctions/ReducerPlugin.scala
diff --git a/src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala b/core/src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala
similarity index 100%
rename from src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala
rename to core/src/main/scala/ap/terfor/conjunctions/SubsumptionRemover.scala
diff --git a/src/main/scala/ap/terfor/equations/ColumnSolver.scala b/core/src/main/scala/ap/terfor/equations/ColumnSolver.scala
similarity index 100%
rename from src/main/scala/ap/terfor/equations/ColumnSolver.scala
rename to core/src/main/scala/ap/terfor/equations/ColumnSolver.scala
diff --git a/src/main/scala/ap/terfor/equations/EquationConj.scala b/core/src/main/scala/ap/terfor/equations/EquationConj.scala
similarity index 100%
rename from src/main/scala/ap/terfor/equations/EquationConj.scala
rename to core/src/main/scala/ap/terfor/equations/EquationConj.scala
diff --git a/src/main/scala/ap/terfor/equations/EquationSet.scala b/core/src/main/scala/ap/terfor/equations/EquationSet.scala
similarity index 100%
rename from src/main/scala/ap/terfor/equations/EquationSet.scala
rename to core/src/main/scala/ap/terfor/equations/EquationSet.scala
diff --git a/src/main/scala/ap/terfor/equations/NegEquationConj.scala b/core/src/main/scala/ap/terfor/equations/NegEquationConj.scala
similarity index 100%
rename from src/main/scala/ap/terfor/equations/NegEquationConj.scala
rename to core/src/main/scala/ap/terfor/equations/NegEquationConj.scala
diff --git a/src/main/scala/ap/terfor/equations/ReduceWithEqs.scala b/core/src/main/scala/ap/terfor/equations/ReduceWithEqs.scala
similarity index 100%
rename from src/main/scala/ap/terfor/equations/ReduceWithEqs.scala
rename to core/src/main/scala/ap/terfor/equations/ReduceWithEqs.scala
diff --git a/src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala b/core/src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala
similarity index 100%
rename from src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala
rename to core/src/main/scala/ap/terfor/equations/ReduceWithNegEqs.scala
diff --git a/src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala b/core/src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala
similarity index 100%
rename from src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala
rename to core/src/main/scala/ap/terfor/inequalities/FMInfsComputer.scala
diff --git a/src/main/scala/ap/terfor/inequalities/InEqConj.scala b/core/src/main/scala/ap/terfor/inequalities/InEqConj.scala
similarity index 100%
rename from src/main/scala/ap/terfor/inequalities/InEqConj.scala
rename to core/src/main/scala/ap/terfor/inequalities/InEqConj.scala
diff --git a/src/main/scala/ap/terfor/inequalities/IntervalProp.scala b/core/src/main/scala/ap/terfor/inequalities/IntervalProp.scala
similarity index 100%
rename from src/main/scala/ap/terfor/inequalities/IntervalProp.scala
rename to core/src/main/scala/ap/terfor/inequalities/IntervalProp.scala
diff --git a/src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala b/core/src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala
similarity index 100%
rename from src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala
rename to core/src/main/scala/ap/terfor/inequalities/ReduceWithInEqs.scala
diff --git a/src/main/scala/ap/terfor/linearcombination/LCBlender.scala b/core/src/main/scala/ap/terfor/linearcombination/LCBlender.scala
similarity index 100%
rename from src/main/scala/ap/terfor/linearcombination/LCBlender.scala
rename to core/src/main/scala/ap/terfor/linearcombination/LCBlender.scala
diff --git a/src/main/scala/ap/terfor/linearcombination/LinearCombination.scala b/core/src/main/scala/ap/terfor/linearcombination/LinearCombination.scala
similarity index 100%
rename from src/main/scala/ap/terfor/linearcombination/LinearCombination.scala
rename to core/src/main/scala/ap/terfor/linearcombination/LinearCombination.scala
diff --git a/src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala b/core/src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala
similarity index 100%
rename from src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala
rename to core/src/main/scala/ap/terfor/linearcombination/ScalingIterator.scala
diff --git a/src/main/scala/ap/terfor/preds/Atom.scala b/core/src/main/scala/ap/terfor/preds/Atom.scala
similarity index 100%
rename from src/main/scala/ap/terfor/preds/Atom.scala
rename to core/src/main/scala/ap/terfor/preds/Atom.scala
diff --git a/src/main/scala/ap/terfor/preds/PredConj.scala b/core/src/main/scala/ap/terfor/preds/PredConj.scala
similarity index 100%
rename from src/main/scala/ap/terfor/preds/PredConj.scala
rename to core/src/main/scala/ap/terfor/preds/PredConj.scala
diff --git a/src/main/scala/ap/terfor/preds/Predicate.scala b/core/src/main/scala/ap/terfor/preds/Predicate.scala
similarity index 100%
rename from src/main/scala/ap/terfor/preds/Predicate.scala
rename to core/src/main/scala/ap/terfor/preds/Predicate.scala
diff --git a/src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala b/core/src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala
similarity index 100%
rename from src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala
rename to core/src/main/scala/ap/terfor/preds/ReduceWithPredLits.scala
diff --git a/src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala b/core/src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala
rename to core/src/main/scala/ap/terfor/substitutions/ComposeSubsts.scala
diff --git a/src/main/scala/ap/terfor/substitutions/ConstantSubst.scala b/core/src/main/scala/ap/terfor/substitutions/ConstantSubst.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/ConstantSubst.scala
rename to core/src/main/scala/ap/terfor/substitutions/ConstantSubst.scala
diff --git a/src/main/scala/ap/terfor/substitutions/IdentitySubst.scala b/core/src/main/scala/ap/terfor/substitutions/IdentitySubst.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/IdentitySubst.scala
rename to core/src/main/scala/ap/terfor/substitutions/IdentitySubst.scala
diff --git a/src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala b/core/src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala
rename to core/src/main/scala/ap/terfor/substitutions/PseudoConstantSubst.scala
diff --git a/src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala b/core/src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala
rename to core/src/main/scala/ap/terfor/substitutions/PseudoDivSubstitution.scala
diff --git a/src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala b/core/src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala
rename to core/src/main/scala/ap/terfor/substitutions/SimpleSubstitution.scala
diff --git a/src/main/scala/ap/terfor/substitutions/Substitution.scala b/core/src/main/scala/ap/terfor/substitutions/Substitution.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/Substitution.scala
rename to core/src/main/scala/ap/terfor/substitutions/Substitution.scala
diff --git a/src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala b/core/src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala
rename to core/src/main/scala/ap/terfor/substitutions/VariableShiftSubst.scala
diff --git a/src/main/scala/ap/terfor/substitutions/VariableSubst.scala b/core/src/main/scala/ap/terfor/substitutions/VariableSubst.scala
similarity index 100%
rename from src/main/scala/ap/terfor/substitutions/VariableSubst.scala
rename to core/src/main/scala/ap/terfor/substitutions/VariableSubst.scala
diff --git a/src/main/scala/ap/theories/ADT.scala b/core/src/main/scala/ap/theories/ADT.scala
similarity index 99%
rename from src/main/scala/ap/theories/ADT.scala
rename to core/src/main/scala/ap/theories/ADT.scala
index 6ffe15709..5fb30ef80 100644
--- a/src/main/scala/ap/theories/ADT.scala
+++ b/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/src/main/scala/ap/theories/BitShiftMultiplication.scala b/core/src/main/scala/ap/theories/BitShiftMultiplication.scala
similarity index 100%
rename from src/main/scala/ap/theories/BitShiftMultiplication.scala
rename to core/src/main/scala/ap/theories/BitShiftMultiplication.scala
diff --git a/src/main/scala/ap/theories/DivZero.scala b/core/src/main/scala/ap/theories/DivZero.scala
similarity index 100%
rename from src/main/scala/ap/theories/DivZero.scala
rename to core/src/main/scala/ap/theories/DivZero.scala
diff --git a/src/main/scala/ap/theories/FunctionalConsistency.scala b/core/src/main/scala/ap/theories/FunctionalConsistency.scala
similarity index 100%
rename from src/main/scala/ap/theories/FunctionalConsistency.scala
rename to core/src/main/scala/ap/theories/FunctionalConsistency.scala
diff --git a/src/main/scala/ap/theories/Incompleteness.scala b/core/src/main/scala/ap/theories/Incompleteness.scala
similarity index 100%
rename from src/main/scala/ap/theories/Incompleteness.scala
rename to core/src/main/scala/ap/theories/Incompleteness.scala
diff --git a/src/main/scala/ap/theories/MulTheory.scala b/core/src/main/scala/ap/theories/MulTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/MulTheory.scala
rename to core/src/main/scala/ap/theories/MulTheory.scala
diff --git a/src/main/scala/ap/theories/SaturationProcedure.scala b/core/src/main/scala/ap/theories/SaturationProcedure.scala
similarity index 100%
rename from src/main/scala/ap/theories/SaturationProcedure.scala
rename to core/src/main/scala/ap/theories/SaturationProcedure.scala
diff --git a/src/main/scala/ap/theories/Theory.scala b/core/src/main/scala/ap/theories/Theory.scala
similarity index 100%
rename from src/main/scala/ap/theories/Theory.scala
rename to core/src/main/scala/ap/theories/Theory.scala
diff --git a/src/main/scala/ap/theories/TheoryBuilder.scala b/core/src/main/scala/ap/theories/TheoryBuilder.scala
similarity index 100%
rename from src/main/scala/ap/theories/TheoryBuilder.scala
rename to core/src/main/scala/ap/theories/TheoryBuilder.scala
diff --git a/src/main/scala/ap/theories/TheoryCollector.scala b/core/src/main/scala/ap/theories/TheoryCollector.scala
similarity index 100%
rename from src/main/scala/ap/theories/TheoryCollector.scala
rename to core/src/main/scala/ap/theories/TheoryCollector.scala
diff --git a/src/main/scala/ap/theories/TheoryRegistry.scala b/core/src/main/scala/ap/theories/TheoryRegistry.scala
similarity index 100%
rename from src/main/scala/ap/theories/TheoryRegistry.scala
rename to core/src/main/scala/ap/theories/TheoryRegistry.scala
diff --git a/src/main/scala/ap/theories/ValueEnumerator.scala b/core/src/main/scala/ap/theories/ValueEnumerator.scala
similarity index 100%
rename from src/main/scala/ap/theories/ValueEnumerator.scala
rename to core/src/main/scala/ap/theories/ValueEnumerator.scala
diff --git a/src/main/scala/ap/theories/arrays/CombArray.scala b/core/src/main/scala/ap/theories/arrays/CombArray.scala
similarity index 100%
rename from src/main/scala/ap/theories/arrays/CombArray.scala
rename to core/src/main/scala/ap/theories/arrays/CombArray.scala
diff --git a/src/main/scala/ap/theories/arrays/ExtArray.scala b/core/src/main/scala/ap/theories/arrays/ExtArray.scala
similarity index 100%
rename from src/main/scala/ap/theories/arrays/ExtArray.scala
rename to core/src/main/scala/ap/theories/arrays/ExtArray.scala
diff --git a/src/main/scala/ap/theories/arrays/MinMaxArray.scala b/core/src/main/scala/ap/theories/arrays/MinMaxArray.scala
similarity index 100%
rename from src/main/scala/ap/theories/arrays/MinMaxArray.scala
rename to core/src/main/scala/ap/theories/arrays/MinMaxArray.scala
diff --git a/src/main/scala/ap/theories/arrays/SetTheory.scala b/core/src/main/scala/ap/theories/arrays/SetTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/arrays/SetTheory.scala
rename to core/src/main/scala/ap/theories/arrays/SetTheory.scala
diff --git a/src/main/scala/ap/theories/arrays/SimpleArray.scala b/core/src/main/scala/ap/theories/arrays/SimpleArray.scala
similarity index 100%
rename from src/main/scala/ap/theories/arrays/SimpleArray.scala
rename to core/src/main/scala/ap/theories/arrays/SimpleArray.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala b/core/src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala
rename to core/src/main/scala/ap/theories/bitvectors/ExtractArithEncoder.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala b/core/src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala
rename to core/src/main/scala/ap/theories/bitvectors/ModCastSplitter.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ModPlugin.scala b/core/src/main/scala/ap/theories/bitvectors/ModPlugin.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ModPlugin.scala
rename to core/src/main/scala/ap/theories/bitvectors/ModPlugin.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala b/core/src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala
rename to core/src/main/scala/ap/theories/bitvectors/ModPostprocessor.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala b/core/src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala
rename to core/src/main/scala/ap/theories/bitvectors/ModPreprocessor.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ModReducer.scala b/core/src/main/scala/ap/theories/bitvectors/ModReducer.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ModReducer.scala
rename to core/src/main/scala/ap/theories/bitvectors/ModReducer.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala b/core/src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala
rename to core/src/main/scala/ap/theories/bitvectors/ModuloArithmetic.scala
diff --git a/src/main/scala/ap/theories/bitvectors/Ring.scala b/core/src/main/scala/ap/theories/bitvectors/Ring.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/Ring.scala
rename to core/src/main/scala/ap/theories/bitvectors/Ring.scala
diff --git a/src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala b/core/src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala
similarity index 100%
rename from src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala
rename to core/src/main/scala/ap/theories/bitvectors/ShiftCastSplitter.scala
diff --git a/src/main/scala/ap/theories/heaps/ArrayHeap.scala b/core/src/main/scala/ap/theories/heaps/ArrayHeap.scala
similarity index 100%
rename from src/main/scala/ap/theories/heaps/ArrayHeap.scala
rename to core/src/main/scala/ap/theories/heaps/ArrayHeap.scala
diff --git a/src/main/scala/ap/theories/heaps/Heap.scala b/core/src/main/scala/ap/theories/heaps/Heap.scala
similarity index 100%
rename from src/main/scala/ap/theories/heaps/Heap.scala
rename to core/src/main/scala/ap/theories/heaps/Heap.scala
diff --git a/src/main/scala/ap/theories/heaps/NativeHeap.scala b/core/src/main/scala/ap/theories/heaps/NativeHeap.scala
similarity index 100%
rename from src/main/scala/ap/theories/heaps/NativeHeap.scala
rename to core/src/main/scala/ap/theories/heaps/NativeHeap.scala
diff --git a/src/main/scala/ap/theories/nia/Buchberger.scala b/core/src/main/scala/ap/theories/nia/Buchberger.scala
similarity index 100%
rename from src/main/scala/ap/theories/nia/Buchberger.scala
rename to core/src/main/scala/ap/theories/nia/Buchberger.scala
diff --git a/core/src/main/scala/ap/theories/nia/Gaussian.scala b/core/src/main/scala/ap/theories/nia/Gaussian.scala
new file mode 100644
index 000000000..b808a4aa3
--- /dev/null
+++ b/core/src/main/scala/ap/theories/nia/Gaussian.scala
@@ -0,0 +1,163 @@
+/**
+ * This file is part of Princess, a theorem prover for Presburger
+ * arithmetic with uninterpreted predicates.
+ * <http://www.philipp.ruemmer.org/princess.shtml>
+ *
+ * Copyright (C)      2014-2019 Philipp Ruemmer <ph_r@gmx.net>
+ *                    2014 Peter Backeman <peter.backeman@it.uu.se>
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * * Redistributions of source code must retain the above copyright notice, this
+ *   list of conditions and the following disclaimer.
+ * 
+ * * Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * 
+ * * Neither the name of the authors nor the names of their
+ *   contributors may be used to endorse or promote products derived from
+ *   this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+package ap.theories.nia
+
+import ap.basetypes.{IdealInt, IdealRat}
+import ap.util.LRUCache
+
+import scala.collection.immutable.BitSet
+
+
+object Gaussian {
+  private val cache = new LRUCache[Vector[Vector[IdealInt]],
+                                   List[(Array[IdealInt], BitSet)]](3)
+
+  def apply(array : Vector[Vector[IdealInt]]) =
+    cache(array) { (new Gaussian(array)).getRows }
+}
+
+
+// Assuming rectangular matrix
+class Gaussian private (array : Vector[Vector[IdealInt]]) {
+  val rows = array.length
+  val cols = array(0).length
+
+  override def toString : String =
+    (for (a <- array) yield a.mkString(" ")).mkString("\n")
+
+  /**
+   * Reduced linear rows with the originating row labels.
+   */
+  val getRows : List[(Array[IdealInt], BitSet)] = {
+    val matrix = Array.tabulate(rows) { r =>
+      Array.tabulate(cols) { c => IdealRat(array(r)(c)) }
+    }
+    val rowComb = Array.tabulate(rows) { r =>
+      Array.tabulate(rows) { c =>
+        if (r == c) IdealRat.ONE else IdealRat.ZERO
+      }
+    }
+
+    var pivotRow = 0
+    var col = 0
+
+    while (pivotRow < rows && col < cols) {
+      var pivot = pivotRow
+      while (pivot < rows && matrix(pivot)(col).isZero)
+        pivot += 1
+
+      if (pivot < rows) {
+        if (pivot != pivotRow) {
+          val tmp = matrix(pivotRow); matrix(pivotRow) = matrix(pivot); matrix(pivot) = tmp
+          val ctmp = rowComb(pivotRow); rowComb(pivotRow) = rowComb(pivot); rowComb(pivot) = ctmp
+        }
+
+        val pivotValue = matrix(pivotRow)(col)
+        var c = col
+        while (c < cols) {
+          matrix(pivotRow)(c) = matrix(pivotRow)(c) / pivotValue
+          c += 1
+        }
+        var l = 0
+        while (l < rows) {
+          rowComb(pivotRow)(l) = rowComb(pivotRow)(l) / pivotValue
+          l += 1
+        }
+
+        var r = 0
+        while (r < rows) {
+          if (r != pivotRow) {
+            val factor = matrix(r)(col)
+            if (!factor.isZero) {
+              c = col
+              while (c < cols) {
+                matrix(r)(c) = matrix(r)(c) - (factor * matrix(pivotRow)(c))
+                c += 1
+              }
+              l = 0
+              while (l < rows) {
+                rowComb(r)(l) = rowComb(r)(l) - (factor * rowComb(pivotRow)(l))
+                l += 1
+              }
+            }
+          }
+          r += 1
+        }
+
+        pivotRow += 1
+      }
+
+      col += 1
+    }
+
+    (for {
+      r <- 0 until rows
+      row = normaliseRow(matrix(r))
+      if row.exists(x => !x.isZero)
+      label = BitSet() ++
+        (for (i <- 0 until rows;
+              if !rowComb(r)(i).isZero)
+         yield i)
+    } yield (row, label)).toList
+  }
+
+  private def normaliseRow(row : Array[IdealRat]) : Array[IdealInt] = {
+    if (row.forall(_.isZero))
+      return Array.fill(cols)(IdealInt.ZERO)
+
+    val lcmDenom =
+      IdealInt.lcm(for (x <- row.iterator; if !x.isZero) yield x.denom)
+
+    val intRow =
+      Array.tabulate(cols) { i =>
+        val x = row(i)
+        if (x.isZero) IdealInt.ZERO else x.num * (lcmDenom / x.denom)
+      }
+
+    val gcdAbs =
+      IdealInt.gcd(for (x <- intRow.iterator; if !x.isZero) yield x.abs)
+
+    if (!gcdAbs.isZero && !gcdAbs.isOne)
+      for (i <- 0 until cols)
+        intRow(i) = intRow(i) / gcdAbs
+
+    val firstNZ = intRow.find(x => !x.isZero)
+    if (firstNZ.exists(_.signum < 0))
+      for (i <- 0 until cols)
+        intRow(i) = -intRow(i)
+
+    intRow
+  }
+}
diff --git a/src/main/scala/ap/theories/nia/GroebnerMultiplication.scala b/core/src/main/scala/ap/theories/nia/GroebnerMultiplication.scala
similarity index 100%
rename from src/main/scala/ap/theories/nia/GroebnerMultiplication.scala
rename to core/src/main/scala/ap/theories/nia/GroebnerMultiplication.scala
diff --git a/src/main/scala/ap/theories/nia/Interval.scala b/core/src/main/scala/ap/theories/nia/Interval.scala
similarity index 100%
rename from src/main/scala/ap/theories/nia/Interval.scala
rename to core/src/main/scala/ap/theories/nia/Interval.scala
diff --git a/src/main/scala/ap/theories/nia/IntervalPropagator.scala b/core/src/main/scala/ap/theories/nia/IntervalPropagator.scala
similarity index 100%
rename from src/main/scala/ap/theories/nia/IntervalPropagator.scala
rename to core/src/main/scala/ap/theories/nia/IntervalPropagator.scala
diff --git a/src/main/scala/ap/theories/nia/Polynomial.scala b/core/src/main/scala/ap/theories/nia/Polynomial.scala
similarity index 100%
rename from src/main/scala/ap/theories/nia/Polynomial.scala
rename to core/src/main/scala/ap/theories/nia/Polynomial.scala
diff --git a/src/main/scala/ap/theories/nia/Splitter.scala b/core/src/main/scala/ap/theories/nia/Splitter.scala
similarity index 100%
rename from src/main/scala/ap/theories/nia/Splitter.scala
rename to core/src/main/scala/ap/theories/nia/Splitter.scala
diff --git a/src/main/scala/ap/theories/package.scala b/core/src/main/scala/ap/theories/package.scala
similarity index 100%
rename from src/main/scala/ap/theories/package.scala
rename to core/src/main/scala/ap/theories/package.scala
diff --git a/src/main/scala/ap/theories/rationals/Fractions.scala b/core/src/main/scala/ap/theories/rationals/Fractions.scala
similarity index 100%
rename from src/main/scala/ap/theories/rationals/Fractions.scala
rename to core/src/main/scala/ap/theories/rationals/Fractions.scala
diff --git a/src/main/scala/ap/theories/rationals/Rationals.scala b/core/src/main/scala/ap/theories/rationals/Rationals.scala
similarity index 100%
rename from src/main/scala/ap/theories/rationals/Rationals.scala
rename to core/src/main/scala/ap/theories/rationals/Rationals.scala
diff --git a/src/main/scala/ap/theories/sequences/ArraySeqTheory.scala b/core/src/main/scala/ap/theories/sequences/ArraySeqTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/sequences/ArraySeqTheory.scala
rename to core/src/main/scala/ap/theories/sequences/ArraySeqTheory.scala
diff --git a/src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala b/core/src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala
similarity index 100%
rename from src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala
rename to core/src/main/scala/ap/theories/sequences/ArraySeqTheoryBuilder.scala
diff --git a/src/main/scala/ap/theories/sequences/SeqTheory.scala b/core/src/main/scala/ap/theories/sequences/SeqTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/sequences/SeqTheory.scala
rename to core/src/main/scala/ap/theories/sequences/SeqTheory.scala
diff --git a/src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala b/core/src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala
similarity index 100%
rename from src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala
rename to core/src/main/scala/ap/theories/sequences/SeqTheoryBuilder.scala
diff --git a/src/main/scala/ap/theories/strings/AbstractStringTheory.scala b/core/src/main/scala/ap/theories/strings/AbstractStringTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/strings/AbstractStringTheory.scala
rename to core/src/main/scala/ap/theories/strings/AbstractStringTheory.scala
diff --git a/src/main/scala/ap/theories/strings/SeqStringTheory.scala b/core/src/main/scala/ap/theories/strings/SeqStringTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/strings/SeqStringTheory.scala
rename to core/src/main/scala/ap/theories/strings/SeqStringTheory.scala
diff --git a/src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala b/core/src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala
similarity index 100%
rename from src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala
rename to core/src/main/scala/ap/theories/strings/SeqStringTheoryBuilder.scala
diff --git a/src/main/scala/ap/theories/strings/StringTheory.scala b/core/src/main/scala/ap/theories/strings/StringTheory.scala
similarity index 100%
rename from src/main/scala/ap/theories/strings/StringTheory.scala
rename to core/src/main/scala/ap/theories/strings/StringTheory.scala
diff --git a/src/main/scala/ap/theories/strings/StringTheoryBuilder.scala b/core/src/main/scala/ap/theories/strings/StringTheoryBuilder.scala
similarity index 100%
rename from src/main/scala/ap/theories/strings/StringTheoryBuilder.scala
rename to core/src/main/scala/ap/theories/strings/StringTheoryBuilder.scala
diff --git a/src/main/scala/ap/types/Sort.scala b/core/src/main/scala/ap/types/Sort.scala
similarity index 100%
rename from src/main/scala/ap/types/Sort.scala
rename to core/src/main/scala/ap/types/Sort.scala
diff --git a/src/main/scala/ap/types/SortedSymbols.scala b/core/src/main/scala/ap/types/SortedSymbols.scala
similarity index 100%
rename from src/main/scala/ap/types/SortedSymbols.scala
rename to core/src/main/scala/ap/types/SortedSymbols.scala
diff --git a/src/main/scala/ap/types/TypeTheory.scala b/core/src/main/scala/ap/types/TypeTheory.scala
similarity index 100%
rename from src/main/scala/ap/types/TypeTheory.scala
rename to core/src/main/scala/ap/types/TypeTheory.scala
diff --git a/src/main/scala/ap/types/UninterpretedSort.scala b/core/src/main/scala/ap/types/UninterpretedSort.scala
similarity index 100%
rename from src/main/scala/ap/types/UninterpretedSort.scala
rename to core/src/main/scala/ap/types/UninterpretedSort.scala
diff --git a/src/main/scala/ap/util/CmdlParser.scala b/core/src/main/scala/ap/util/CmdlParser.scala
similarity index 100%
rename from src/main/scala/ap/util/CmdlParser.scala
rename to core/src/main/scala/ap/util/CmdlParser.scala
diff --git a/src/main/scala/ap/util/Combinatorics.scala b/core/src/main/scala/ap/util/Combinatorics.scala
similarity index 100%
rename from src/main/scala/ap/util/Combinatorics.scala
rename to core/src/main/scala/ap/util/Combinatorics.scala
diff --git a/src/main/scala/ap/util/CountIt.scala b/core/src/main/scala/ap/util/CountIt.scala
similarity index 100%
rename from src/main/scala/ap/util/CountIt.scala
rename to core/src/main/scala/ap/util/CountIt.scala
diff --git a/src/main/scala/ap/util/Debug.scala b/core/src/main/scala/ap/util/Debug.scala
similarity index 100%
rename from src/main/scala/ap/util/Debug.scala
rename to core/src/main/scala/ap/util/Debug.scala
diff --git a/src/main/scala/ap/util/Dijkstra.scala b/core/src/main/scala/ap/util/Dijkstra.scala
similarity index 100%
rename from src/main/scala/ap/util/Dijkstra.scala
rename to core/src/main/scala/ap/util/Dijkstra.scala
diff --git a/src/main/scala/ap/util/FastImmutableMap.scala b/core/src/main/scala/ap/util/FastImmutableMap.scala
similarity index 100%
rename from src/main/scala/ap/util/FastImmutableMap.scala
rename to core/src/main/scala/ap/util/FastImmutableMap.scala
diff --git a/src/main/scala/ap/util/FilterIt.scala b/core/src/main/scala/ap/util/FilterIt.scala
similarity index 100%
rename from src/main/scala/ap/util/FilterIt.scala
rename to core/src/main/scala/ap/util/FilterIt.scala
diff --git a/src/main/scala/ap/util/LRUCache.scala b/core/src/main/scala/ap/util/LRUCache.scala
similarity index 100%
rename from src/main/scala/ap/util/LRUCache.scala
rename to core/src/main/scala/ap/util/LRUCache.scala
diff --git a/src/main/scala/ap/util/LazyIndexedSeqConcat.scala b/core/src/main/scala/ap/util/LazyIndexedSeqConcat.scala
similarity index 100%
rename from src/main/scala/ap/util/LazyIndexedSeqConcat.scala
rename to core/src/main/scala/ap/util/LazyIndexedSeqConcat.scala
diff --git a/src/main/scala/ap/util/LazyIndexedSeqSlice.scala b/core/src/main/scala/ap/util/LazyIndexedSeqSlice.scala
similarity index 100%
rename from src/main/scala/ap/util/LazyIndexedSeqSlice.scala
rename to core/src/main/scala/ap/util/LazyIndexedSeqSlice.scala
diff --git a/src/main/scala/ap/util/LazyMappedMap.scala b/core/src/main/scala/ap/util/LazyMappedMap.scala
similarity index 100%
rename from src/main/scala/ap/util/LazyMappedMap.scala
rename to core/src/main/scala/ap/util/LazyMappedMap.scala
diff --git a/src/main/scala/ap/util/LazyMappedSet.scala b/core/src/main/scala/ap/util/LazyMappedSet.scala
similarity index 100%
rename from src/main/scala/ap/util/LazyMappedSet.scala
rename to core/src/main/scala/ap/util/LazyMappedSet.scala
diff --git a/src/main/scala/ap/util/Logic.scala b/core/src/main/scala/ap/util/Logic.scala
similarity index 100%
rename from src/main/scala/ap/util/Logic.scala
rename to core/src/main/scala/ap/util/Logic.scala
diff --git a/src/main/scala/ap/util/OpCounters.scala b/core/src/main/scala/ap/util/OpCounters.scala
similarity index 100%
rename from src/main/scala/ap/util/OpCounters.scala
rename to core/src/main/scala/ap/util/OpCounters.scala
diff --git a/src/main/scala/ap/util/POGraph.scala b/core/src/main/scala/ap/util/POGraph.scala
similarity index 100%
rename from src/main/scala/ap/util/POGraph.scala
rename to core/src/main/scala/ap/util/POGraph.scala
diff --git a/src/main/scala/ap/util/PeekIterator.scala b/core/src/main/scala/ap/util/PeekIterator.scala
similarity index 100%
rename from src/main/scala/ap/util/PeekIterator.scala
rename to core/src/main/scala/ap/util/PeekIterator.scala
diff --git a/src/main/scala/ap/util/PlainRange.scala b/core/src/main/scala/ap/util/PlainRange.scala
similarity index 100%
rename from src/main/scala/ap/util/PlainRange.scala
rename to core/src/main/scala/ap/util/PlainRange.scala
diff --git a/src/main/scala/ap/util/PriorityQueueWithIterators.scala b/core/src/main/scala/ap/util/PriorityQueueWithIterators.scala
similarity index 100%
rename from src/main/scala/ap/util/PriorityQueueWithIterators.scala
rename to core/src/main/scala/ap/util/PriorityQueueWithIterators.scala
diff --git a/src/main/scala/ap/util/RuntimeStatistics.scala b/core/src/main/scala/ap/util/RuntimeStatistics.scala
similarity index 100%
rename from src/main/scala/ap/util/RuntimeStatistics.scala
rename to core/src/main/scala/ap/util/RuntimeStatistics.scala
diff --git a/src/main/scala/ap/util/Seqs.scala b/core/src/main/scala/ap/util/Seqs.scala
similarity index 100%
rename from src/main/scala/ap/util/Seqs.scala
rename to core/src/main/scala/ap/util/Seqs.scala
diff --git a/src/main/scala/ap/util/Tarjan.scala b/core/src/main/scala/ap/util/Tarjan.scala
similarity index 100%
rename from src/main/scala/ap/util/Tarjan.scala
rename to core/src/main/scala/ap/util/Tarjan.scala
diff --git a/src/main/scala/ap/util/Timeout.scala b/core/src/main/scala/ap/util/Timeout.scala
similarity index 100%
rename from src/main/scala/ap/util/Timeout.scala
rename to core/src/main/scala/ap/util/Timeout.scala
diff --git a/src/main/scala/ap/util/Timer.scala b/core/src/main/scala/ap/util/Timer.scala
similarity index 100%
rename from src/main/scala/ap/util/Timer.scala
rename to core/src/main/scala/ap/util/Timer.scala
diff --git a/src/main/scala/ap/util/UnionMap.scala b/core/src/main/scala/ap/util/UnionMap.scala
similarity index 100%
rename from src/main/scala/ap/util/UnionMap.scala
rename to core/src/main/scala/ap/util/UnionMap.scala
diff --git a/src/main/scala/ap/util/UnionSet.scala b/core/src/main/scala/ap/util/UnionSet.scala
similarity index 100%
rename from src/main/scala/ap/util/UnionSet.scala
rename to core/src/main/scala/ap/util/UnionSet.scala
diff --git a/src/test/scala/ap/basetypes/TestIdealInt.scala b/core/src/test/scala/ap/basetypes/TestIdealInt.scala
similarity index 100%
rename from src/test/scala/ap/basetypes/TestIdealInt.scala
rename to core/src/test/scala/ap/basetypes/TestIdealInt.scala
diff --git a/src/test/scala/ap/basetypes/TestLeftistHeap.scala b/core/src/test/scala/ap/basetypes/TestLeftistHeap.scala
similarity index 100%
rename from src/test/scala/ap/basetypes/TestLeftistHeap.scala
rename to core/src/test/scala/ap/basetypes/TestLeftistHeap.scala
diff --git a/src/test/scala/ap/basetypes/TestSetTrie.scala b/core/src/test/scala/ap/basetypes/TestSetTrie.scala
similarity index 100%
rename from src/test/scala/ap/basetypes/TestSetTrie.scala
rename to core/src/test/scala/ap/basetypes/TestSetTrie.scala
diff --git a/core/src/test/scala/ap/core/ImplicationCheckerTest.scala b/core/src/test/scala/ap/core/ImplicationCheckerTest.scala
new file mode 100644
index 000000000..80d364bfb
--- /dev/null
+++ b/core/src/test/scala/ap/core/ImplicationCheckerTest.scala
@@ -0,0 +1,46 @@
+package ap.core
+
+import ap.parser.IExpression._
+import ap.terfor.ConstantTerm
+
+import org.scalacheck.Properties
+
+class ImplicationCheckerTest extends Properties("ImplicationChecker") {
+
+  private def c(name : String) = new ConstantTerm(name)
+
+  property("decrease-is-strict") = {
+    val n = c("n")
+    ImplicationChecker.implies(
+      Seq(i(n) > 0),
+      i(n) - 1 < i(n)
+    )
+  }
+
+  property("decrease-keeps-nonnegative") = {
+    val current = c("current")
+    val next = c("next")
+    ImplicationChecker.implies(
+      Seq(i(current) > 0,
+          i(next) === i(current) - 1),
+      i(next) >= 0
+    )
+  }
+
+  property("invalid-implication-is-rejected") = {
+    val n = c("n")
+    !ImplicationChecker.implies(
+      Seq(i(n) >= 0),
+      i(n) - 1 >= 0
+    )
+  }
+
+  property("strict-upper-bound-step") = {
+    val iVar = c("i")
+    val hi = c("hi")
+    ImplicationChecker.implies(
+      Seq(i(iVar) < i(hi)),
+      i(iVar) + 1 <= i(hi)
+    )
+  }
+}
diff --git a/src/test/scala/ap/parser/SimplePrint.scala b/core/src/test/scala/ap/parser/SimplePrint.scala
similarity index 100%
rename from src/test/scala/ap/parser/SimplePrint.scala
rename to core/src/test/scala/ap/parser/SimplePrint.scala
diff --git a/src/test/scala/ap/parser/TestInputAbsyVisitor.scala b/core/src/test/scala/ap/parser/TestInputAbsyVisitor.scala
similarity index 100%
rename from src/test/scala/ap/parser/TestInputAbsyVisitor.scala
rename to core/src/test/scala/ap/parser/TestInputAbsyVisitor.scala
diff --git a/src/test/scala/ap/parser/TestSimplifier.scala b/core/src/test/scala/ap/parser/TestSimplifier.scala
similarity index 100%
rename from src/test/scala/ap/parser/TestSimplifier.scala
rename to core/src/test/scala/ap/parser/TestSimplifier.scala
diff --git a/src/test/scala/ap/proof/TestEquationSystems.scala b/core/src/test/scala/ap/proof/TestEquationSystems.scala
similarity index 100%
rename from src/test/scala/ap/proof/TestEquationSystems.scala
rename to core/src/test/scala/ap/proof/TestEquationSystems.scala
diff --git a/src/test/scala/ap/proof/TestRandomProving.scala b/core/src/test/scala/ap/proof/TestRandomProving.scala
similarity index 100%
rename from src/test/scala/ap/proof/TestRandomProving.scala
rename to core/src/test/scala/ap/proof/TestRandomProving.scala
diff --git a/src/test/scala/ap/terfor/TestGenConjunctions.scala b/core/src/test/scala/ap/terfor/TestGenConjunctions.scala
similarity index 100%
rename from src/test/scala/ap/terfor/TestGenConjunctions.scala
rename to core/src/test/scala/ap/terfor/TestGenConjunctions.scala
diff --git a/src/test/scala/ap/terfor/TestPropConnectives.scala b/core/src/test/scala/ap/terfor/TestPropConnectives.scala
similarity index 100%
rename from src/test/scala/ap/terfor/TestPropConnectives.scala
rename to core/src/test/scala/ap/terfor/TestPropConnectives.scala
diff --git a/src/test/scala/ap/terfor/TestTermOrder.scala b/core/src/test/scala/ap/terfor/TestTermOrder.scala
similarity index 100%
rename from src/test/scala/ap/terfor/TestTermOrder.scala
rename to core/src/test/scala/ap/terfor/TestTermOrder.scala
diff --git a/src/test/scala/ap/terfor/equations/TestEquationSet.scala b/core/src/test/scala/ap/terfor/equations/TestEquationSet.scala
similarity index 100%
rename from src/test/scala/ap/terfor/equations/TestEquationSet.scala
rename to core/src/test/scala/ap/terfor/equations/TestEquationSet.scala
diff --git a/src/test/scala/ap/terfor/inequalities/TestInequalities.scala b/core/src/test/scala/ap/terfor/inequalities/TestInequalities.scala
similarity index 100%
rename from src/test/scala/ap/terfor/inequalities/TestInequalities.scala
rename to core/src/test/scala/ap/terfor/inequalities/TestInequalities.scala
diff --git a/src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala b/core/src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala
similarity index 100%
rename from src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala
rename to core/src/test/scala/ap/terfor/linearcombination/TestLinearCombination.scala
diff --git a/src/test/scala/ap/terfor/substitutions/TestSubst.scala b/core/src/test/scala/ap/terfor/substitutions/TestSubst.scala
similarity index 100%
rename from src/test/scala/ap/terfor/substitutions/TestSubst.scala
rename to core/src/test/scala/ap/terfor/substitutions/TestSubst.scala
diff --git a/src/test/scala/ap/theories/DivModEncoding.scala b/core/src/test/scala/ap/theories/DivModEncoding.scala
similarity index 100%
rename from src/test/scala/ap/theories/DivModEncoding.scala
rename to core/src/test/scala/ap/theories/DivModEncoding.scala
diff --git a/core/src/test/scala/ap/util/Prop.scala b/core/src/test/scala/ap/util/Prop.scala
new file mode 100644
index 000000000..6570e881a
--- /dev/null
+++ b/core/src/test/scala/ap/util/Prop.scala
@@ -0,0 +1,82 @@
+/**
+ * This file is part of Princess, a theorem prover for Presburger
+ * arithmetic with uninterpreted predicates.
+ * <http://www.philipp.ruemmer.org/princess.shtml>
+ *
+ * Copyright (C) 2024 Philipp Ruemmer <ph_r@gmx.net>
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are met:
+ * 
+ * * Redistributions of source code must retain the above copyright notice, this
+ *   list of conditions and the following disclaimer.
+ * 
+ * * Redistributions in binary form must reproduce the above copyright notice,
+ *   this list of conditions and the following disclaimer in the documentation
+ *   and/or other materials provided with the distribution.
+ * 
+ * * Neither the name of the authors nor the names of their
+ *   contributors may be used to endorse or promote products derived from
+ *   this software without specific prior written permission.
+ * 
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+ * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+ * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+ * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+ * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+ * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+ * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ */
+
+package ap.util
+
+import java.io.{ByteArrayOutputStream, PrintStream}
+
+import org.scalacheck.Properties
+
+object Prop {
+
+  def assertEquals(a : Any, b : Any) : Unit =
+    assert(a == b)
+
+  def assertEquals(msg : String, a : Any, b : Any) : Unit =
+    assert(a == b, msg)
+
+  def assertTrue(b : Boolean) : Unit =
+    assert(b)
+
+  def assertTrue(msg : String, b : Boolean) : Unit =
+    assert(b, msg)
+
+}
+
+trait ExtraAssertions extends Properties {
+
+  def checkOutput(expected : String)(comp : => Unit) : Boolean = {
+    val output = {
+      val baos = new ByteArrayOutputStream
+      val ps = new PrintStream(baos)
+      Console.withOut(ps)(comp)
+      ps.flush()
+      baos.toString
+    }
+
+    if (output == expected) {
+      true
+    } else if (expected == "") {
+      println(output)
+      false
+    } else {
+      for (((exp, seen), line) <-
+             (expected.linesIterator zip output.linesIterator).zipWithIndex) {
+        if (exp != seen)
+          Console.err.println(f"${name}:${line}: ${seen}")
+      }
+      false
+    }
+  }
+
+}
diff --git a/src/main/scala/ap/parser/SMTParser2InputAbsy.scala b/src/main/scala/ap/parser/SMTParser2InputAbsy.scala
index 03eb37a90..b87a7148d 100644
--- a/src/main/scala/ap/parser/SMTParser2InputAbsy.scala
+++ b/src/main/scala/ap/parser/SMTParser2InputAbsy.scala
@@ -69,15 +69,13 @@ object SMTParser2InputAbsy {
   import IExpression.{Sort => TSort}
   import SMTTypes._
 
-  protected[parser] def toNormalBool(s : TSort) : TSort = s match {
-    case TSort.MultipleValueBool => TSort.Bool
-    case s => s
-  }
+  type SMTFunctionType = SMTSupport.SMTFunctionType
+  val SMTFunctionType = SMTSupport.SMTFunctionType
 
-  case class SMTFunctionType(arguments : List[SMTType],
-                             result : SMTType)
+  protected[parser] def toNormalBool(s : TSort) : TSort =
+    SMTSupport.toNormalBool(s)
 
-  val SMTBoolVariableType = SMTFunctionType(List(), SMTBool)
+  val SMTBoolVariableType : SMTFunctionType = SMTSupport.SMTBoolVariableType
 
   sealed abstract class VariableType
   case class BoundVariable(varType : SMTType)              extends VariableType
diff --git a/src/main/scala/ap/theories/nia/Gaussian.scala b/src/main/scala/ap/theories/nia/Gaussian.scala
index 727926952..2b57d4853 100644
--- a/src/main/scala/ap/theories/nia/Gaussian.scala
+++ b/src/main/scala/ap/theories/nia/Gaussian.scala
@@ -36,10 +36,9 @@ package ap.theories.nia
 
 import ap.basetypes.IdealInt
 import ap.terfor.linearcombination.LinearCombination
-import ap.terfor.{TerForConvenience, TermOrder, ConstantTerm}
-import ap.terfor.preds.Atom
-import ap.terfor.equations.EquationConj
+import ap.terfor.ConstantTerm
 import ap.terfor.TerForConvenience._
+import ap.terfor.equations.EquationConj
 import ap.SimpleAPI
 import ap.parser._
 import ap.util.{Debug, LRUCache}