From b7cc66f3334c92c195b17d70417845b128d784ff Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Thu, 25 Mar 2021 21:39:12 +0100
Subject: [PATCH 01/27] fixed case of character classes starting with a -

---
 src/main/scala/ostrich/ECMARegexParser.scala | 4 ++++
 src/test/scala/SMTLIBTests.scala             | 2 ++
 tests/parse-ecma-bug2.smt2                   | 7 +++++++
 3 files changed, 13 insertions(+)
 create mode 100644 tests/parse-ecma-bug2.smt2

diff --git a/src/main/scala/ostrich/ECMARegexParser.scala b/src/main/scala/ostrich/ECMARegexParser.scala
index 7b9b0aaa93..c261990313 100644
--- a/src/main/scala/ostrich/ECMARegexParser.scala
+++ b/src/main/scala/ostrich/ECMARegexParser.scala
@@ -365,6 +365,10 @@ class ECMARegexParser(theory : OstrichStringTheory) {
       toSingleCharRegex(printer print p)
     override def visit(p : ecma2020regex.Absyn.NegAtom, arg : VisitorArg) =
       toSingleCharRegex(printer print p)
+    override def visit(p : ecma2020regex.Absyn.NegAtomND, arg : VisitorArg) =
+      toSingleCharRegex(printer print p)
+    override def visit(p : ecma2020regex.Absyn.DashAtomNN, arg : VisitorArg) =
+      toSingleCharRegex(printer print p)
     
     override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg1, arg : VisitorArg)=
       toSingleCharRegex(p.normalchar_)
diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
index 1c51a057e2..99e416c78f 100644
--- a/src/test/scala/SMTLIBTests.scala
+++ b/src/test/scala/SMTLIBTests.scala
@@ -225,6 +225,8 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
     checkFile("tests/parse-ecma-cases.smt2", "unsat")
   property("parse-ecma-bug1.smt2") =
     checkFile("tests/parse-ecma-bug1.smt2", "sat")
+  property("parse-ecma-bug2.smt2") =
+    checkFile("tests/parse-ecma-bug2.smt2", "unsat")
 
   property("parse-regex-lookahead.smt2") =
     checkFile("tests/parse-regex-lookahead.smt2", "sat")
diff --git a/tests/parse-ecma-bug2.smt2 b/tests/parse-ecma-bug2.smt2
new file mode 100644
index 0000000000..0f442a960d
--- /dev/null
+++ b/tests/parse-ecma-bug2.smt2
@@ -0,0 +1,7 @@
+
+(declare-const w String)
+(assert (str.in.re w (re.from_ecma2020 '^[-a]')))
+
+(assert (= w ""))
+
+(check-sat)

From 29bd540587c9aa696b3060473279a0eba9043fd3 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Mon, 29 Mar 2021 20:11:35 +0200
Subject: [PATCH 02/27] optimized formula reduction; add a [+-]minimizeAutomata
 flag to choose whether automata constructed from regular expressions should
 be minized

---
 ostrich                                       |  2 +-
 ostrich-client                                |  2 +-
 src/main/scala/ostrich/AutDatabase.scala      | 54 ++++++++++++++++++-
 src/main/scala/ostrich/OFlags.scala           | 10 ++--
 src/main/scala/ostrich/OstrichReducer.scala   | 14 +++--
 .../scala/ostrich/OstrichStringTheory.scala   |  2 +-
 .../ostrich/OstrichStringTheoryBuilder.scala  | 11 ++--
 src/main/scala/ostrich/Regex2Aut.scala        |  5 +-
 src/test/scala/SMTLIBTests.scala              |  3 ++
 tests/minimize-problem.smt2                   |  8 +++
 10 files changed, 91 insertions(+), 20 deletions(-)
 create mode 100644 tests/minimize-problem.smt2

diff --git a/ostrich b/ostrich
index 1cee60275a..fc8e92f3a0 100755
--- a/ostrich
+++ b/ostrich
@@ -20,7 +20,7 @@ ostrichParams=""
 
 for p; do
     case "$p" in
-        [+-]eager | [+-]forward | -length=*)
+        [+-]eager | [+-]forward | -length=* | [+-]minimizeAutomata)
             if [ x"$ostrichParams" = x"" ]; then
                 ostrichParams=$p
             else
diff --git a/ostrich-client b/ostrich-client
index 748879fd1a..f737a15de0 100755
--- a/ostrich-client
+++ b/ostrich-client
@@ -88,7 +88,7 @@ until [ $success -eq 0 ]; do
 
         for var; do
 	    case "$var" in
-                [+-]eager | [+-]forward | -length=*)
+                [+-]eager | [+-]forward | -length=* | [+-]minimizeAutomata)
                     if [ x"$ostrichParams" = x"" ]; then
                         ostrichParams=$var
                     else
diff --git a/src/main/scala/ostrich/AutDatabase.scala b/src/main/scala/ostrich/AutDatabase.scala
index 3a3f52cfa5..4e142b69db 100644
--- a/src/main/scala/ostrich/AutDatabase.scala
+++ b/src/main/scala/ostrich/AutDatabase.scala
@@ -57,7 +57,8 @@ object AutDatabase {
  * regular expressions. The database will assign a unique id to regular
  * expressions, and will compute the resulting automaton on demand.
  */
-class AutDatabase(theory : OstrichStringTheory) {
+class AutDatabase(theory : OstrichStringTheory,
+                  minimizeAutomata : Boolean) {
 
   import AutDatabase._
 
@@ -100,7 +101,7 @@ class AutDatabase(theory : OstrichStringTheory) {
         case None =>
           (id2Regex get id) match {
             case Some(regex) => {
-              val aut = regex2Aut buildAut regex
+              val aut = regex2Aut.buildAut(regex, minimizeAutomata)
               id2Aut.put(id, aut)
               Some(aut)
             }
@@ -110,6 +111,13 @@ class AutDatabase(theory : OstrichStringTheory) {
       }
     }
 
+  /**
+   * Query the automaton that belongs to the regular expression with given id;
+   * return the automaton only if it is already in the database.
+   */
+  def id2AutomatonBE(id : Int) : Option[Automaton] =
+    synchronized { id2Aut get id }
+
   /**
    * Query the complemented automaton that belongs to the regular
    * expression with given id.
@@ -131,6 +139,14 @@ class AutDatabase(theory : OstrichStringTheory) {
       }
     }
 
+  /**
+   * Query the complemented automaton that belongs to the regular
+   * expression with given id;
+   * return the automaton only if it is already in the database.
+   */
+  def id2ComplementedAutomatonBE(id : Int) : Option[Automaton] =
+    synchronized { id2CompAut get id }
+
   /**
    * Query the automaton that belongs to the regular expression with
    * given id.
@@ -140,6 +156,16 @@ class AutDatabase(theory : OstrichStringTheory) {
     case ComplementedAut(id) => id2ComplementedAutomaton(id)
   }
 
+  /**
+   * Query the automaton that belongs to the regular expression with
+   * given id;
+   * return the automaton only if it is already in the database.
+   */
+  def id2AutomatonBE(id : NamedAutomaton) : Option[Automaton] = id match {
+    case PositiveAut(id)     => id2AutomatonBE(id)
+    case ComplementedAut(id) => id2ComplementedAutomatonBE(id)
+  }
+
   /**
    * Check whether <code>aut1</code> specifies a subset of <code>aut2</code>.
    */
@@ -160,6 +186,30 @@ class AutDatabase(theory : OstrichStringTheory) {
       true
     }
 
+  /**
+   * Check whether <code>aut1</code> specifies a subset of <code>aut2</code>;
+   * the check is only carried out when all required automata are already in
+   * the database.
+   */
+  def isSubsetOfBE(aut1 : NamedAutomaton,
+                   aut2 : NamedAutomaton) : Option[Boolean] =
+    if (aut1.id < aut2.id) {
+      synchronized {
+        // aut1 <= aut2
+        //  <==>
+        // (aut1 & aut2.complement) = empty
+        for (a1 <- id2AutomatonBE(aut1);
+             a2 <- id2AutomatonBE(aut2.complement)) yield 
+          subsetRel.getOrElseUpdate((aut1, aut2),
+                                    !AutomataUtils.areConsistentAutomata(
+                                      List(a1, a2)))
+      }
+    } else if (aut1.id > aut2.id) {
+      isSubsetOfBE(aut2.complement, aut1.complement)
+    } else {
+      Some(true)
+    }
+
   /**
    * Check whether <code>aut1</code> and <code>aut2</code> have empty
    * intersection.
diff --git a/src/main/scala/ostrich/OFlags.scala b/src/main/scala/ostrich/OFlags.scala
index d80bce49e6..f46bab692b 100644
--- a/src/main/scala/ostrich/OFlags.scala
+++ b/src/main/scala/ostrich/OFlags.scala
@@ -1,6 +1,6 @@
 /**
  * This file is part of Ostrich, an SMT solver for strings.
- * Copyright (c) 2018-2020 Matthew Hague, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2018-2021 Matthew Hague, Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -44,8 +44,10 @@ case class OFlags(
 
   // Pre-image specific options
   eagerAutomataOperations : Boolean = false,
-  measureTimes : Boolean = false,
-  useLength : OFlags.LengthOptions.Value = OFlags.LengthOptions.Auto,
-  forwardApprox : Boolean = false
+  measureTimes            : Boolean = false,
+  useLength               : OFlags.LengthOptions.Value =
+                                      OFlags.LengthOptions.Auto,
+  forwardApprox           : Boolean = false,
+  minimizeAutomata        : Boolean = false
 
 )
diff --git a/src/main/scala/ostrich/OstrichReducer.scala b/src/main/scala/ostrich/OstrichReducer.scala
index efffe226db..5e64dfc2dd 100644
--- a/src/main/scala/ostrich/OstrichReducer.scala
+++ b/src/main/scala/ostrich/OstrichReducer.scala
@@ -275,7 +275,7 @@ class OstrichReducer protected[ostrich]
 
           val newPos, newNeg, curPos, curNeg = new ArrayBuffer[Atom]
 
-          import autDatabase.{isSubsetOf, emptyIntersection}
+          import autDatabase.{isSubsetOf, isSubsetOfBE, emptyIntersection}
 
           def pickNextTerm : Term =
             if (posIt.hasNext) {
@@ -298,22 +298,26 @@ class OstrichReducer protected[ostrich]
 
           def isFwdSubsumed(aut : NamedAutomaton) : Boolean =
             (curPos exists { a =>
-               isSubsetOf(PositiveAut(regexAtomToId(a)), aut) }) ||
+               isSubsetOfBE(PositiveAut(regexAtomToId(a)), aut) ==
+               Some(true) }) ||
             (curNeg exists { a =>
-               isSubsetOf(ComplementedAut(regexAtomToId(a)), aut) })
+               isSubsetOfBE(ComplementedAut(regexAtomToId(a)), aut) ==
+               Some(true) })
 
           def removeBwdSubsumed(aut : NamedAutomaton) : Unit = {
             var n = 0
 
             while (n < curPos.size)
-              if (isSubsetOf(aut, PositiveAut(regexAtomToId(curPos(n)))))
+              if (isSubsetOfBE(aut, PositiveAut(regexAtomToId(curPos(n)))) ==
+                    Some(true))
                 curPos remove n
               else
                 n = n + 1
 
             n = 0
             while (n < curNeg.size)
-              if (isSubsetOf(aut, ComplementedAut(regexAtomToId(curNeg(n)))))
+              if (isSubsetOfBE(aut, ComplementedAut(regexAtomToId(curNeg(n))))==
+                    Some(true))
                 curNeg remove n
               else
                 n = n + 1
diff --git a/src/main/scala/ostrich/OstrichStringTheory.scala b/src/main/scala/ostrich/OstrichStringTheory.scala
index 9fc8ded921..14c8456e85 100644
--- a/src/main/scala/ostrich/OstrichStringTheory.scala
+++ b/src/main/scala/ostrich/OstrichStringTheory.scala
@@ -154,7 +154,7 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
 
   //////////////////////////////////////////////////////////////////////////////
 
-  val autDatabase = new AutDatabase(this)
+  val autDatabase = new AutDatabase(this, flags.minimizeAutomata)
 
   val str_in_re_id =
     MonoSortedPredicate("str.in.re.id", List(StringSort, Sort.Integer))
diff --git a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
index e367e5c17a..20788364d0 100644
--- a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
+++ b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
@@ -48,19 +48,21 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder {
     println
     println("Loading " + name + ", a solver for string constraints")
     println("(c) Matthew Hague, Philipp Rümmer, 2018-2021")
-    println("With contributions by Riccardo de Masellis.")
+    println("With contributions by Riccardo De Masellis.")
     println("For more information, see https://github.com/uuverifiers/ostrich")
     println
   }
 
   def setAlphabetSize(w : Int) : Unit = ()
 
-  private var eager, forward = false
+  private var eager, forward, minimizeAuts = false
   private var useLen : OFlags.LengthOptions.Value = OFlags.LengthOptions.Auto
 
   override def parseParameter(str : String) : Unit = str match {
     case CmdlParser.Opt("eager", value) =>
       eager = value
+    case CmdlParser.Opt("minimizeAutomata", value) =>
+      minimizeAuts = value
     case CmdlParser.ValueOpt("length", "off") =>
       useLen = OFlags.LengthOptions.Off
     case CmdlParser.ValueOpt("length", "on") =>
@@ -103,8 +105,9 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder {
 
     new OstrichStringTheory (symTransducers,
                              OFlags(eagerAutomataOperations = eager,
-                                    useLength = useLen,
-                                    forwardApprox = forward))
+                                    useLength               = useLen,
+                                    forwardApprox           = forward,
+                                    minimizeAutomata        = minimizeAuts))
   }
 
 }
diff --git a/src/main/scala/ostrich/Regex2Aut.scala b/src/main/scala/ostrich/Regex2Aut.scala
index 6e25ff347e..228b056653 100644
--- a/src/main/scala/ostrich/Regex2Aut.scala
+++ b/src/main/scala/ostrich/Regex2Aut.scala
@@ -455,8 +455,9 @@ class Regex2Aut(theory : OstrichStringTheory) {
   def buildBricsAut(t : ITerm) : BAutomaton =
     toBAutomaton(t, true)
 
-  def buildAut(t : ITerm) : AtomicStateAutomaton =
-    new BricsAutomaton(toBAutomaton(t, true))
+  def buildAut(t : ITerm,
+               minimize : Boolean = true) : AtomicStateAutomaton =
+    new BricsAutomaton(toBAutomaton(t, minimize))
 
   private def numToUnicode(num : Int) : String =
     new String(Character.toChars(num))
diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
index 99e416c78f..9031068e88 100644
--- a/src/test/scala/SMTLIBTests.scala
+++ b/src/test/scala/SMTLIBTests.scala
@@ -54,6 +54,9 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
   property("case-insensitive-2.smt2") =
     checkFile("tests/case-insensitive-2.smt2", "unsat")
 
+  property("minimize-problem.smt2") =
+    checkFile("tests/minimize-problem.smt2", "sat")
+
   property("str.from_int.smt2") =
     checkFile("tests/str.from_int.smt2", "sat")
   property("str.from_int_2.smt2") =
diff --git a/tests/minimize-problem.smt2 b/tests/minimize-problem.smt2
new file mode 100644
index 0000000000..7a9d51cbe6
--- /dev/null
+++ b/tests/minimize-problem.smt2
@@ -0,0 +1,8 @@
+; Example that tends to time out when trying to minimize/determinize automata
+
+(declare-const w String)
+(assert (str.in.re w (re.from_ecma2020 "^.+@.+\\..{2,20}$")))
+
+(assert (str.in.re w (re.* (re.range "\u{20}" "\u{FFFF}"))))
+
+(check-sat)

From 648161b34f5462a27c70d4d05e2f46636ac3149e Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Thu, 8 Apr 2021 14:59:54 +0200
Subject: [PATCH 03/27] handle large strings defined using define-fun correctly

---
 src/main/scala/ostrich/Regex2Aut.scala   | 23 +++++++++--------------
 src/main/scala/ostrich/StrDatabase.scala | 16 ++++++++++++++++
 2 files changed, 25 insertions(+), 14 deletions(-)

diff --git a/src/main/scala/ostrich/Regex2Aut.scala b/src/main/scala/ostrich/Regex2Aut.scala
index 228b056653..07c52147b4 100644
--- a/src/main/scala/ostrich/Regex2Aut.scala
+++ b/src/main/scala/ostrich/Regex2Aut.scala
@@ -152,35 +152,30 @@ class Regex2Aut(theory : OstrichStringTheory) {
 
   //////////////////////////////////////////////////////////////////////////////
 
+  import theory.strDatabase.EncodedString
+
   private def toBAutomaton(t : ITerm,
                            minimize : Boolean) : BAutomaton = t match {
     case IFunApp(`re_charrange`,
     Seq(SmartConst(IdealInt(a)), SmartConst(IdealInt(b)))) =>
       BasicAutomata.makeCharRange(a.toChar, b.toChar)
 
-    case IFunApp(`str_to_re`, Seq(a)) => {
-      // modified by Riccardo
-      a match {
-        case IIntLit(value) =>
-          BasicAutomata.makeString(theory.strDatabase.id2Str(value.intValueSafe))
-        case _ =>
-          BasicAutomata.makeString(StringTheory.term2String(a))
-      }
-    }
+    case IFunApp(`str_to_re`, Seq(EncodedString(str))) =>
+      BasicAutomata.makeString(str)
 
-    case IFunApp(`re_from_str`, Seq(a)) => {
+    case IFunApp(`re_from_str`, Seq(EncodedString(str))) => {
       // TODO: this translation has to be checked more carefully, there might
       // be problems due to escaping. The processing of regexes can also
       // only be done correctly within a proper regex parser.
   
-      val bricsPattern = jsRegex2BricsRegex(StringTheory.term2String(a))
+      val bricsPattern = jsRegex2BricsRegex(str)
       new RegExp(bricsPattern).toAutomaton(minimize)
     }
 
-    case IFunApp(`re_from_ecma2020`, Seq(a)) => {
+    case IFunApp(`re_from_ecma2020`, Seq(EncodedString(str))) => {
       val parser = new ECMARegexParser(theory)
-      val t = parser.string2Term(StringTheory.term2String(a))
-      toBAutomaton(t, minimize)
+      val s = parser.string2Term(str)
+      toBAutomaton(s, minimize)
     }
 
     case IFunApp(`re_case_insensitive`, Seq(a)) => {
diff --git a/src/main/scala/ostrich/StrDatabase.scala b/src/main/scala/ostrich/StrDatabase.scala
index 23926d6efc..a5e730f2b4 100644
--- a/src/main/scala/ostrich/StrDatabase.scala
+++ b/src/main/scala/ostrich/StrDatabase.scala
@@ -162,4 +162,20 @@ class StrDatabase(theory : OstrichStringTheory) {
                                 id
                               })
   }
+
+  /**
+   * Extractor to recognise strings in different representations.
+   */
+  object EncodedString {
+    def unapply(t : ITerm) : Option[String] =
+      t match {
+        case IIntLit(IdealInt(value)) =>
+          Some(id2Str(value))
+        case StringTheory.ConcreteString(str) =>
+          Some(str)
+        case _ =>
+          None
+      }
+  }
+
 }

From 6388893b923b9cd7c1b5a02850aabfe855abcaae Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Mon, 19 Apr 2021 15:28:27 +0200
Subject: [PATCH 04/27] error message

---
 src/main/scala/ostrich/ECMARegexParser.scala | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/ostrich/ECMARegexParser.scala b/src/main/scala/ostrich/ECMARegexParser.scala
index c261990313..5c42c2093e 100644
--- a/src/main/scala/ostrich/ECMARegexParser.scala
+++ b/src/main/scala/ostrich/ECMARegexParser.scala
@@ -49,7 +49,9 @@ class ECMARegexParser(theory : OstrichStringTheory) {
 
   def string2Term(inputString : String) : ITerm = {
     val pat = parseRegex(inputString)
-    TranslationVisitor(pat)
+    val res = TranslationVisitor(pat)
+    println(res)
+    res
   }
 
   def parseRegex(inputString : String) : Pattern = {
@@ -521,6 +523,8 @@ class ECMARegexParser(theory : OstrichStringTheory) {
     case (IFunApp(`re_charrange`, Seq(Const(lower), _)),
           IFunApp(`re_charrange`, Seq(_, Const(upper)))) =>
       re_charrange(lower, upper)
+    case _ =>
+      throw new Exception("Illformed character range in a regular expression")
   }
 
   private def parseDecimalDigits(digits : Seq[DecimalDigit]) : IdealInt =

From 5fffc224aeb01bd845f516c0b1fbd833512a27d4 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Thu, 22 Apr 2021 10:26:29 +0200
Subject: [PATCH 05/27] removed a left-over println

---
 src/main/scala/ostrich/ECMARegexParser.scala | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/main/scala/ostrich/ECMARegexParser.scala b/src/main/scala/ostrich/ECMARegexParser.scala
index 5c42c2093e..c0c85c777a 100644
--- a/src/main/scala/ostrich/ECMARegexParser.scala
+++ b/src/main/scala/ostrich/ECMARegexParser.scala
@@ -49,9 +49,7 @@ class ECMARegexParser(theory : OstrichStringTheory) {
 
   def string2Term(inputString : String) : ITerm = {
     val pat = parseRegex(inputString)
-    val res = TranslationVisitor(pat)
-    println(res)
-    res
+    TranslationVisitor(pat)
   }
 
   def parseRegex(inputString : String) : Pattern = {

From 6a603389244330718ac8dbb5fe47c30842509955 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Thu, 22 Apr 2021 14:19:12 +0200
Subject: [PATCH 06/27] support for octal escape sequences

---
 build.sbt                                    |   2 +-
 src/main/scala/ostrich/ECMARegexParser.scala | 156 +++++++++++++------
 tests/parse-ecma-cases.smt2                  |   8 +
 3 files changed, 121 insertions(+), 45 deletions(-)

diff --git a/build.sbt b/build.sbt
index bf4dd1f960..c9fb15c5b4 100644
--- a/build.sbt
+++ b/build.sbt
@@ -8,7 +8,7 @@ lazy val commonSettings = Seq(
   scalacOptions += "-deprecation",
   resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/").withAllowInsecureProtocol(true),
   libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT",
-  libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.4-SNAPSHOT",
+  libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.5",
   libraryDependencies += "org.sat4j" % "org.sat4j.core" % "2.3.1",
   libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.0" % "test",
   libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8"
diff --git a/src/main/scala/ostrich/ECMARegexParser.scala b/src/main/scala/ostrich/ECMARegexParser.scala
index c0c85c777a..8970e30067 100644
--- a/src/main/scala/ostrich/ECMARegexParser.scala
+++ b/src/main/scala/ostrich/ECMARegexParser.scala
@@ -41,10 +41,18 @@ import ecma2020regex.Absyn.{Quantifier => ECMAQuantifier}
 
 import scala.collection.JavaConversions.{asScalaBuffer, asScalaIterator}
 
+object ECMARegexParser {
+
+  val OctalEscape = """[0-7]{1,3}""".r
+
+}
+
 class ECMARegexParser(theory : OstrichStringTheory) {
 
   import theory._
   import IExpression._
+  import ECMARegexParser._
+
   val printer = new PrettyPrinterNonStatic
 
   def string2Term(inputString : String) : ITerm = {
@@ -289,99 +297,125 @@ class ECMARegexParser(theory : OstrichStringTheory) {
       EPS
     }
 
-    override def visit(p : ecma2020regex.Absyn.EndAnchor, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.EndAnchor,
+                       arg : VisitorArg) = {
       Console.err.println("Warning: ignoring anchor $")
       EPS
     }
 
-    override def visit(p : ecma2020regex.Absyn.WordAnchor, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.WordAnchor,
+                       arg : VisitorArg) =
       WordBoundary()
 
-    override def visit(p : ecma2020regex.Absyn.NonWordAnchor, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.NonWordAnchor,
+                       arg : VisitorArg) =
       NonWordBoundary()
 
-    override def visit(p : ecma2020regex.Absyn.NegClass, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.NegClass,
+                       arg : VisitorArg) =
       charComplement(p.classrangesc_.accept(this, arg))
 
-    override def visit(p : ecma2020regex.Absyn.EmptyRange, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.EmptyRange,
+                       arg : VisitorArg) =
       NONE
 
-    override def visit(p : ecma2020regex.Absyn.ClassCont, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.ClassCont,
+                       arg : VisitorArg) = {
       val left = p.classatomc_.accept(this, arg)
       val rest = p.neclassrangesnodashc_.accept(this, arg)
       reUnion(left, rest)
     }
 
-    override def visit(p : ecma2020regex.Absyn.ClassCharRange, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.ClassCharRange,
+                       arg : VisitorArg) = {
       val r = regexRange(p.classatomc_1.accept(this, arg),
                          p.classatomc_2.accept(this, arg))
       val rest = p.classrangesc_.accept(this, arg)
       reUnion(r, rest)
     }
 
-    override def visit(p : ecma2020regex.Absyn.ClassContNN, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.ClassContNN,
+                       arg : VisitorArg) = {
       val left = p.classatomnonegc_.accept(this, arg)
       val rest = p.neclassrangesnodashc_.accept(this, arg)
       reUnion(left, rest)
     }
 
-    override def visit(p : ecma2020regex.Absyn.ClassCharRangeNN, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.ClassCharRangeNN,
+                       arg : VisitorArg) = {
       val r = regexRange(p.classatomnonegc_.accept(this, arg),
                          p.classatomc_.accept(this, arg))
       val rest = p.classrangesc_.accept(this, arg)
       reUnion(r, rest)
     }
 
-    override def visit(p : ecma2020regex.Absyn.ClassContND, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.ClassContND,
+                       arg : VisitorArg) = {
       val left = p.classatomnodashc_.accept(this, arg)
       val rest = p.neclassrangesnodashc_.accept(this, arg)
       reUnion(left, rest)
     }
 
-    override def visit(p : ecma2020regex.Absyn.ClassCharRangeND, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.ClassCharRangeND,
+                       arg : VisitorArg) = {
       val r = regexRange(p.classatomnodashc_.accept(this, arg),
                          p.classatomc_.accept(this, arg))
       val rest = p.classrangesc_.accept(this, arg)
       reUnion(r, rest)
     }
 
-    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter1, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter1,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter2, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter2,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter3, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter3,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter4, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.SyntaxCharacter4,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
 
-    override def visit(p : ecma2020regex.Absyn.NormalCharPat, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.NormalCharPat,
+                       arg : VisitorArg) =
       toSingleCharRegex(p.normalchar_)
-    override def visit(p : ecma2020regex.Absyn.DecimalDigitPat, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.DecimalDigitPat,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.DashPat, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.DashPat,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
 
-    override def visit(p : ecma2020regex.Absyn.DashAtom, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.DashAtom,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.NegAtom, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.NegAtom,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.NegAtomND, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.NegAtomND,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.DashAtomNN, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.DashAtomNN,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
     
-    override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg1, arg : VisitorArg)=
+    override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg1,
+                       arg : VisitorArg)=
       toSingleCharRegex(p.normalchar_)
-    override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg2, arg : VisitorArg)=
+    override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg2,
+                       arg : VisitorArg)=
       toSingleCharRegex(printer print p)
-    override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg3, arg : VisitorArg)=
+    override def visit(p : ecma2020regex.Absyn.ClassAtomNoDashNeg3,
+                       arg : VisitorArg)=
       toSingleCharRegex(printer print p)
 
     // Different escape sequences
 
-    override def visit(p : ecma2020regex.Absyn.DecAtomEscape, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.DecAtomEscape,
+                       arg : VisitorArg) = {
       val firstDigit =
-        p.positivedecimal_
+        printer print p.decimaldigit_
       val tailDigits =
         p.maybedecimaldigits_ match {
           case _ : NoDecimalDigits => ""
@@ -389,53 +423,87 @@ class ECMARegexParser(theory : OstrichStringTheory) {
             (for (d <- ds.listdecimaldigit_)
              yield (printer print d)).mkString("")
         }
-      val captureGroupNum = IdealInt(firstDigit + tailDigits)
-      Console.err.println("Warning: over-approximating back-reference as .*")
-      ALL
+      val allDigits =
+        firstDigit + tailDigits
+
+      allDigits match {
+        case OctalEscape() =>
+          charSet(Integer.parseInt(allDigits, 8))
+        case _ => {
+          val captureGroupNum = IdealInt(allDigits)
+          Console.err.println(
+            "Warning: over-approximating back-reference as re.any")
+          ALL
+        }
+      }
     }
 
-    override def visit(p : ecma2020regex.Absyn.BClassEscape, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.BClassEscape,
+                       arg : VisitorArg) =
       charSet(0x0008)
-    override def visit(p : ecma2020regex.Absyn.DashClassEscape, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.DashClassEscape,
+                       arg : VisitorArg) =
       charSet(0x002D)
-    override def visit(p : ecma2020regex.Absyn.NullCharEscape, arg : VisitorArg) =
-      charSet(0x0000)
 
-    override def visit(p : ecma2020regex.Absyn.LetterCharEscape, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.LetterCharEscape,
+                       arg : VisitorArg) = {
       val letter = printer print p.controlletter_
       assert(letter.size == 1)
       charSet(letter(0).toInt % 32)
     }
 
-    override def visit(p : ecma2020regex.Absyn.ControlEscapeT, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.ControlEscapeT,
+                       arg : VisitorArg) =
       charSet(0x0009)
-    override def visit(p : ecma2020regex.Absyn.ControlEscapeN, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.ControlEscapeN,
+                       arg : VisitorArg) =
       charSet(0x000A)
-    override def visit(p : ecma2020regex.Absyn.ControlEscapeV, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.ControlEscapeV,
+                       arg : VisitorArg) =
       charSet(0x000B)
-    override def visit(p : ecma2020regex.Absyn.ControlEscapeF, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.ControlEscapeF,
+                       arg : VisitorArg) =
       charSet(0x000C)
-    override def visit(p : ecma2020regex.Absyn.ControlEscapeR, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.ControlEscapeR,
+                       arg : VisitorArg) =
       charSet(0x000D)
 
-    override def visit(p : ecma2020regex.Absyn.HexEscapeSequence, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.HexEscapeSequence,
+                       arg : VisitorArg) =
       charSet(Integer.parseInt((printer print p.hexdigit_1) +
                                  (printer print p.hexdigit_2), 16))
 
-    override def visit(p : ecma2020regex.Absyn.Hex4UniEscapeSequence, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.Hex4UniEscapeSequence,
+                       arg : VisitorArg) =
       charSet(Integer.parseInt((printer print p.hexdigit_1) +
                                  (printer print p.hexdigit_2) +
                                  (printer print p.hexdigit_3) +
                                  (printer print p.hexdigit_4), 16))
 
-    override def visit(p : ecma2020regex.Absyn.CodepointUniEscapeSequence, arg : VisitorArg) = {
+    override def visit(p : ecma2020regex.Absyn.CodepointUniEscapeSequence,
+                       arg : VisitorArg) = {
       val str = printer print p
       charSet(Integer.parseInt(str.substring(2, str.size - 1), 16))
     }
 
-    override def visit(p : ecma2020regex.Absyn.IdentityEscape, arg : VisitorArg) =
+    override def visit(p : ecma2020regex.Absyn.IdentityEscape,
+                       arg : VisitorArg) =
       toSingleCharRegex(printer print p)
 
+    override def visit(p : ecma2020regex.Absyn.OctClassEscape1,
+                       arg : VisitorArg) =
+      charSet(Integer.parseInt(printer print p.octaldigit_, 8))
+
+    override def visit(p : ecma2020regex.Absyn.OctClassEscape2,
+                       arg : VisitorArg) =
+      charSet(Integer.parseInt((printer print p.octaldigit_1) +
+                               (printer print p.octaldigit_2), 8))
+
+    override def visit(p : ecma2020regex.Absyn.OctClassEscape3,
+                       arg : VisitorArg) =
+      charSet(Integer.parseInt((printer print p.octaldigit_1) +
+                               (printer print p.octaldigit_2) +
+                               (printer print p.octaldigit_3), 8))
   }
 
   //////////////////////////////////////////////////////////////////////////////
diff --git a/tests/parse-ecma-cases.smt2 b/tests/parse-ecma-cases.smt2
index 417b3c62f3..27638b2e73 100644
--- a/tests/parse-ecma-cases.smt2
+++ b/tests/parse-ecma-cases.smt2
@@ -52,6 +52,14 @@
            (and (str.in_re w (re.from_ecma2020 '[ a]*'))
                 (not (str.prefixof "a" w))))
 
+        (= (str.in_re w (re.from_ecma2020 '\74abc\076'))
+           (str.in_re w (str.to.re "<abc>")))
+
+        (= (str.in_re w (re.from_ecma2020 '[^\0744\76]*'))
+           (and (not (str.contains w "<"))
+                (not (str.contains w ">"))
+                (not (str.contains w "4"))))
+
  )))
 
 (check-sat)

From 7bb930343f73c81aa7fad1ed8b6e7690c5f3c1e6 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Thu, 6 May 2021 16:02:23 +0200
Subject: [PATCH 07/27] added missing cases

---
 src/main/scala/ostrich/TransducerTranslator.scala | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/ostrich/TransducerTranslator.scala b/src/main/scala/ostrich/TransducerTranslator.scala
index fe2233d790..4ec9070f47 100644
--- a/src/main/scala/ostrich/TransducerTranslator.scala
+++ b/src/main/scala/ostrich/TransducerTranslator.scala
@@ -1,6 +1,6 @@
 /**
  * This file is part of Ostrich, an SMT solver for strings.
- * Copyright (c) 2018-2020 Matthew Hague, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2018-2021 Matthew Hague, Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -145,6 +145,10 @@ object TransducerTranslator {
                   lBound = Some(bound.intValueSafe.toChar)
                 case Geq(Const(bound), `inputC`) =>
                   uBound = Some(bound.intValueSafe.toChar)
+                case INot(Geq(`inputC`, Const(bound))) => // inputC < bound
+                  uBound = Some((bound.intValueSafe - 1).toChar)
+                case INot(Geq(Const(bound), `inputC`)) => // bound < inputC
+                  lBound = Some((bound.intValueSafe + 1).toChar)
                 case EqLit(`inputC`, value) => {
                   lBound = Some(value.intValueSafe.toChar)
                   uBound = Some(value.intValueSafe.toChar)

From 9a1bc3838a68d33aa24ade4762150b4b5407a837 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Mon, 10 May 2021 21:27:07 +0200
Subject: [PATCH 08/27] better handling of prefixof, substr

---
 src/main/scala/ostrich/AutDatabase.scala      | 16 +++++++-
 src/main/scala/ostrich/BricsAutomaton.scala   | 25 +++++++++++-
 src/main/scala/ostrich/BricsTransducer.scala  | 40 ++++++++++++++++++-
 .../scala/ostrich/OstrichPreprocessor.scala   | 22 ++++++++++
 src/main/scala/ostrich/OstrichReducer.scala   | 32 ++++++++++++---
 src/main/scala/ostrich/OstrichSolver.scala    |  5 +++
 .../OstrichStringFunctionTranslator.scala     | 14 ++++++-
 .../scala/ostrich/OstrichStringTheory.scala   | 12 ++++--
 src/test/scala/SMTLIBTests.scala              |  4 ++
 tests/substring2.smt2                         | 13 ++++++
 tests/substring2b.smt2                        | 13 ++++++
 11 files changed, 181 insertions(+), 15 deletions(-)
 create mode 100644 tests/substring2.smt2
 create mode 100644 tests/substring2b.smt2

diff --git a/src/main/scala/ostrich/AutDatabase.scala b/src/main/scala/ostrich/AutDatabase.scala
index 4e142b69db..78573e7495 100644
--- a/src/main/scala/ostrich/AutDatabase.scala
+++ b/src/main/scala/ostrich/AutDatabase.scala
@@ -64,6 +64,8 @@ class AutDatabase(theory : OstrichStringTheory,
 
   private val regex2Aut  = new Regex2Aut(theory)
 
+  private var nextId     = 0
+
   private val regexes    = new MHashMap[ITerm, Int]
   private val id2Regex   = new MHashMap[Int, ITerm]
   private val id2Aut     = new MHashMap[Int, Automaton]
@@ -78,11 +80,23 @@ class AutDatabase(theory : OstrichStringTheory,
   def regex2Id(regexTerm : ITerm) : Int =
     synchronized {
       regexes.getOrElseUpdate(regexTerm, {
-                                val id = regexes.size
+                                val id = nextId
+                                nextId = nextId + 1
                                 id2Regex.put(id, regexTerm)
                                 id })
     }
 
+  /**
+   * Add a new automaton to the database.
+   */
+  def automaton2Id(aut : Automaton) : Int =
+    synchronized {
+      val id = nextId
+      nextId = nextId + 1
+      id2Aut.put(id, aut)
+      id
+    }
+
   /**
    * Query the id of a regular expression.
    */
diff --git a/src/main/scala/ostrich/BricsAutomaton.scala b/src/main/scala/ostrich/BricsAutomaton.scala
index ff65a90a26..beccd8e355 100644
--- a/src/main/scala/ostrich/BricsAutomaton.scala
+++ b/src/main/scala/ostrich/BricsAutomaton.scala
@@ -1,6 +1,6 @@
 /**
  * This file is part of Ostrich, an SMT solver for strings.
- * Copyright (c) 2018-2020 Matthew Hague, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2018-2021 Matthew Hague, Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -69,6 +69,29 @@ object BricsAutomaton {
   def fromString(str : String) : BricsAutomaton =
     new BricsAutomaton(BasicAutomata makeString str)
 
+  /**
+   * Build brics automaton that accepts exactly the prefixes of the given
+   * string.
+   */
+  def prefixAutomaton(str : String) : BricsAutomaton = {
+    val builder = new BricsAutomatonBuilder
+
+    val states =
+      (for (n <- 0 to str.size) yield builder.getNewState).toIndexedSeq
+
+    builder setInitialState states(0)
+
+    for ((c, n) <- str.iterator.zipWithIndex)
+      builder.addTransition(states(n),
+                            builder.LabelOps singleton c,
+                            states(n+1))
+
+    for (s <- states)
+      builder.setAccept(s, true)
+
+    builder.getAutomaton
+  }
+
   /**
    * A new automaton that accepts any string
    */
diff --git a/src/main/scala/ostrich/BricsTransducer.scala b/src/main/scala/ostrich/BricsTransducer.scala
index 5280dfc21a..28685c7e37 100644
--- a/src/main/scala/ostrich/BricsTransducer.scala
+++ b/src/main/scala/ostrich/BricsTransducer.scala
@@ -1,6 +1,6 @@
 /**
  * This file is part of Ostrich, an SMT solver for strings.
- * Copyright (c) 2018-2020 Matthew Hague, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2018-2021 Matthew Hague, Philipp Ruemmer. All rights reserved.
  * 
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
@@ -90,6 +90,44 @@ object BricsTransducer {
         })
     }
 
+  /**
+   * Construct a transducer that removes the first <code>trimLeft</code>
+   * and the last <code>trimRight</code> characters of a string.
+   */
+  def getTrimTransducer(trimLeft : Int, trimRight : Int) : BricsTransducer = {
+    assert(trimLeft >= 0 && trimRight >= 0)
+
+    import Transducer._
+ 
+    val builder = BricsTransducer.getBuilder
+
+    val delStates =
+      for (i <- 0 to (trimLeft + trimRight)) yield builder.getNewState
+    val copyStates =
+      for (i <- 0 to trimRight) yield builder.getNewState
+
+    for (Seq(s1, s2) <- (delStates sliding 2) ++ (copyStates sliding 2))
+      builder.addTransition(s1,
+                            builder.LabelOps.sigmaLabel,
+                            OutputOp("", NOP, ""),
+                            s2)
+
+    for (s <- List(delStates(trimLeft), copyStates.head))
+      builder.addTransition(s,
+                            builder.LabelOps.sigmaLabel,
+                            OutputOp("", Plus(0), ""),
+                            copyStates.head)
+
+    builder.setInitialState(delStates(0))
+
+    for (s <- delStates)
+      builder.setAccept(s, true)
+
+    builder.setAccept(copyStates.last, true)
+
+    builder.getTransducer
+  }
+
   /**
    * Transducer that eats every input and produces no output.
    */
diff --git a/src/main/scala/ostrich/OstrichPreprocessor.scala b/src/main/scala/ostrich/OstrichPreprocessor.scala
index 5115caab02..a2c4a99e7c 100644
--- a/src/main/scala/ostrich/OstrichPreprocessor.scala
+++ b/src/main/scala/ostrich/OstrichPreprocessor.scala
@@ -86,12 +86,15 @@ class OstrichPreprocessor(theory : OstrichStringTheory)
       val asRE = re_++(str_to_re(subStr), re_all())
       str_in_re(bigStr, asRE)
     }
+
+/*
     case (IAtom(`str_prefixof`, _),
           Seq(subStr : ITerm, bigStr : ITerm)) if ctxt.polarity < 0 => {
       val s = VariableShiftVisitor(subStr, 0, 1)
       val t = VariableShiftVisitor(bigStr, 0, 1)
       StringSort.ex(str_++(s, v(0, StringSort)) === t)
     }
+ */
 
     case (IAtom(`str_suffixof`, _),
           Seq(subStr@ConcreteString(_), bigStr : ITerm)) => {
@@ -133,6 +136,25 @@ class OstrichPreprocessor(theory : OstrichStringTheory)
       )))
     }
 
+    case (IFunApp(`str_substr`, _),
+          Seq(bigStr : ITerm,
+              Const(begin),
+              Difference(IFunApp(`str_len`, Seq(bigStr2)), Const(end))))
+        if bigStr == bigStr2 && begin.signum >= 0 && end >= begin =>
+      str_trim(bigStr, begin, end - begin)
+
+      // TODO: need proper condition for length
+/*
+    case (IFunApp(`str_substr`, _),
+          Seq(bigStr : ITerm,
+              begin : ITerm,
+              Difference(IFunApp(`str_len`, Seq(bigStr2)), end : ITerm)))
+        if bigStr == bigStr2 =>
+      ite(begin >= 0,
+          str_trim(bigStr, begin, end - begin),
+          "")
+ */
+
     case (IFunApp(`str_substr`, _),
           Seq(bigStr : ITerm, begin : ITerm, len : ITerm)) => {
       val shBigStr3 = VariableShiftVisitor(bigStr, 0, 3)
diff --git a/src/main/scala/ostrich/OstrichReducer.scala b/src/main/scala/ostrich/OstrichReducer.scala
index 5e64dfc2dd..445ed0100a 100644
--- a/src/main/scala/ostrich/OstrichReducer.scala
+++ b/src/main/scala/ostrich/OstrichReducer.scala
@@ -82,7 +82,7 @@ class OstrichReducerFactory protected[ostrich] (theory : OstrichStringTheory)
       extends ReducerPluginFactory {
   import OstrichReducer.extractLanguageConstraints
 
-  import theory.{str_len, int_to_str, str_to_int, FunPred}
+  import theory.{str_len, int_to_str, str_to_int, str_prefixof, FunPred}
 
   def apply(conj : Conjunction, order : TermOrder) =
     new OstrichReducer(theory,
@@ -90,9 +90,9 @@ class OstrichReducerFactory protected[ostrich] (theory : OstrichStringTheory)
                        List(extractLanguageConstraints(conj.predConj, theory)),
                        this)
 
-  val _str_len    = FunPred(str_len)
-  val _int_to_str = FunPred(int_to_str)
-  val _str_to_int = FunPred(str_to_int)
+  val _str_len      = FunPred(str_len)
+  val _int_to_str   = FunPred(int_to_str)
+  val _str_to_int   = FunPred(str_to_int)
 }
 
 /**
@@ -108,7 +108,9 @@ class OstrichReducer protected[ostrich]
 
   import OstrichReducer._
   import theory.{_str_empty, _str_cons, _str_++,
-                 str_empty, str_cons, str_in_re_id, strDatabase, autDatabase}
+                 str_empty, str_cons, str_in_re_id, str_prefixof,
+                 re_++, str_to_re, re_all,
+                 strDatabase, autDatabase}
   import factory.{_str_len, _int_to_str, _str_to_int}
 
   def passQuantifiers(num : Int) = this
@@ -158,7 +160,8 @@ class OstrichReducer protected[ostrich]
     ReducerPlugin.rewritePreds(predConj,
                                List(_str_empty, _str_cons,
                                     str_in_re_id, _str_len,
-                                    _int_to_str, _str_to_int) ++
+                                    _int_to_str, _str_to_int,
+                                    str_prefixof) ++
                                  funTranslator.translatablePredicates,
                                order,
                                logger) { a =>
@@ -234,6 +237,23 @@ class OstrichReducer protected[ostrich]
             a
           }
 
+        case `str_prefixof` =>
+          if (isConcrete(a(0))) {
+            assert(a(0).isConstant)
+            val asRE  = IFunApp(re_++,
+                                List(IFunApp(str_to_re, List(a(0).constant)),
+                                     IFunApp(re_all, List())))
+            val autId = autDatabase.regex2Id(asRE)
+            str_in_re_id(List(a(1), l(autId)))
+          } else if (isConcrete(a(1))) {
+            val str   = strDatabase.term2Str(a(1)).get
+            val autId = autDatabase.automaton2Id(
+                          BricsAutomaton.prefixAutomaton(str))
+            str_in_re_id(List(a(0), l(autId)))
+          } else {
+            a
+          }
+
         case p => {
           assert(funTranslator.translatablePredicates contains p)
           funTranslator(a) match {
diff --git a/src/main/scala/ostrich/OstrichSolver.scala b/src/main/scala/ostrich/OstrichSolver.scala
index 99f89fddbd..4b93c46b68 100644
--- a/src/main/scala/ostrich/OstrichSolver.scala
+++ b/src/main/scala/ostrich/OstrichSolver.scala
@@ -54,6 +54,7 @@ class OstrichSolver(theory : OstrichStringTheory,
                  str_in_re_id, str_to_re, re_from_str, re_from_ecma2020,
                  re_case_insensitive,
                  str_replace, str_replacere, str_replaceall, str_replaceallre,
+                 str_prefixof,
                  re_none, re_all, re_allchar, re_charrange,
                  re_++, re_union, re_inter, re_diff, re_*, re_+, re_opt,
                  re_comp, re_loop, re_eps, FunPred, strDatabase}
@@ -146,6 +147,10 @@ class OstrichSolver(theory : OstrichStringTheory,
         if (a(1).isZero)
           regexes += ((a(0), BricsAutomaton fromString ""))
       }
+      case `str_prefixof` => {
+        val rightVar = theory.StringSort.newConstant("rhs")
+        funApps += ((ConcatPreOp, List(a(0), rightVar), a(1)))
+      }
       case FunPred(f) if rexOps contains f =>
         // nothing
       case p if (theory.predicates contains p) =>
diff --git a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
index bfa9551018..501df91eb8 100644
--- a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
+++ b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
@@ -44,7 +44,7 @@ import ap.basetypes.IdealInt
 class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
                                       facts : Conjunction) {
   import theory.{FunPred, strDatabase, autDatabase,
-                 str_++, str_at,
+                 str_++, str_at, str_trim,
                  str_replaceall, str_replace,
                  str_replaceallre, str_replacere}
 
@@ -52,7 +52,7 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
 
   val translatablePredicates : Seq[Predicate] =
     (for (f <- List(str_++, str_replace, str_replaceall,
-                    str_replacere, str_replaceallre, str_at) ++
+                    str_replacere, str_replaceallre, str_at, str_trim) ++
                theory.extraFunctionPreOps.keys)
      yield FunPred(f)) ++ theory.transducerPreOps.keys
   
@@ -92,10 +92,20 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
     case FunPred(`str_at`) => {
       val op = () => {
         val LinearCombination.Constant(IdealInt(ind)) = a(1)
+        // TODO: generate length information
         TransducerPreOp(BricsTransducer.getStrAtTransducer(ind))
       }
       Some((op, List(a(0)), a(2)))
     }
+    case FunPred(`str_trim`) => {
+      val op = () => {
+        val LinearCombination.Constant(IdealInt(trimLeft))  = a(1)
+        val LinearCombination.Constant(IdealInt(trimRight)) = a(2)
+        // TODO: generate length information
+        TransducerPreOp(BricsTransducer.getTrimTransducer(trimLeft, trimRight))
+      }
+      Some((op, List(a(0)), a(3)))
+    }
     case FunPred(f) if theory.extraFunctionPreOps contains f => {
       val (op, argSelector, resSelector) = theory.extraFunctionPreOps(f)
       Some((() => op, argSelector(a), resSelector(a)))
diff --git a/src/main/scala/ostrich/OstrichStringTheory.scala b/src/main/scala/ostrich/OstrichStringTheory.scala
index 14c8456e85..1188ffe7e5 100644
--- a/src/main/scala/ostrich/OstrichStringTheory.scala
+++ b/src/main/scala/ostrich/OstrichStringTheory.scala
@@ -122,6 +122,9 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
     MonoSortedIFunction("re.from_ecma2020", List(SSo), RSo, true, false)
   val re_case_insensitive =
     MonoSortedIFunction("re.case_insensitive", List(RSo), RSo, true, false)
+  val str_trim =
+    MonoSortedIFunction("str.trim",
+                        List(SSo, Sort.Integer, Sort.Integer), SSo, true, false)
 
   // List of user-defined functions on strings that can be extended
   val extraStringFunctions : Seq[(String, IFunction, PreOp,
@@ -147,8 +150,9 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
       yield (name, Left(f))) ++
      (for ((name, p, _) <- transducersWithPreds.iterator)
       yield (name, Right(p))) ++
-     Iterator((re_from_ecma2020.name, Left(re_from_ecma2020)),
-              (re_case_insensitive.name, Left(re_case_insensitive)))).toMap
+     Iterator((re_from_ecma2020.name,    Left(re_from_ecma2020)),
+              (re_case_insensitive.name, Left(re_case_insensitive)),
+              (str_trim.name,            Left(str_trim)))).toMap
 
   val extraIndexedOps : Map[(String, Int), Either[IFunction, Predicate]] = Map()
 
@@ -168,7 +172,7 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
   val functions =
     predefFunctions ++ List(str_empty, str_cons, str_head, str_tail) ++
     (extraStringFunctions map (_._2)) ++
-    List(re_from_ecma2020, re_case_insensitive)
+    List(re_from_ecma2020, re_case_insensitive, str_trim)
 
   val (funPredicates, _, _, functionPredicateMap) =
     Theory.genAxioms(theoryFunctions = functions,
@@ -201,7 +205,7 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
 
   // Set of the predicates that are fully supported at this point
   private val supportedPreds : Set[Predicate] =
-    Set(str_in_re, str_in_re_id) ++
+    Set(str_in_re, str_in_re_id, str_prefixof) ++
     (for (f <- Set(str_empty, str_cons, str_at,
                    str_++, str_replace, str_replaceall,
                    str_replacere, str_replaceallre, str_to_re,
diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
index 9031068e88..aa5dcf1bfc 100644
--- a/src/test/scala/SMTLIBTests.scala
+++ b/src/test/scala/SMTLIBTests.scala
@@ -212,6 +212,10 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
     checkFile("tests/substring.smt2", "sat")
   property("substring-bug.smt2") =
     checkFile("tests/substring-bug.smt2", "sat")
+  property("substring2.smt2") =
+    checkFile("tests/substring2.smt2", "unsat")
+  property("substring2b.smt2") =
+    checkFile("tests/substring2b.smt2", "sat")
 
   property("parse-regex.smt2") =
     checkFile("tests/parse-regex.smt2", "sat")
diff --git a/tests/substring2.smt2 b/tests/substring2.smt2
new file mode 100644
index 0000000000..a132e24fd4
--- /dev/null
+++ b/tests/substring2.smt2
@@ -0,0 +1,13 @@
+
+(set-logic QF_S)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= x (str.++ "x" z)))
+(assert (= y (str.substr x 3 (- (str.len x) 5))))
+(assert (str.in_re y (re.from_ecma2020 'a+b+')))
+(assert (= (str.at x 4) "c"))
+
+(check-sat)
\ No newline at end of file
diff --git a/tests/substring2b.smt2 b/tests/substring2b.smt2
new file mode 100644
index 0000000000..c7c81ffde9
--- /dev/null
+++ b/tests/substring2b.smt2
@@ -0,0 +1,13 @@
+
+(set-logic QF_S)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= x (str.++ "x" z)))
+(assert (= y (str.substr x 3 (- (str.len x) 5))))
+(assert (str.in_re y (re.from_ecma2020 'a+b+')))
+(assert (= (str.at x 5) "c"))
+
+(check-sat)
\ No newline at end of file

From 77de50cf258b9846657feb289d1d53fe2f9a888b Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Mon, 10 May 2021 22:42:21 +0200
Subject: [PATCH 09/27] handling of further str.at cases

---
 src/main/scala/ostrich/BricsTransducer.scala  | 52 ++++++++++++++++++-
 .../scala/ostrich/OstrichPreprocessor.scala   |  8 +++
 .../OstrichStringFunctionTranslator.scala     | 13 ++++-
 .../scala/ostrich/OstrichStringTheory.scala   |  6 ++-
 src/test/scala/SMTLIBTests.scala              |  6 +++
 tests/str.at-3.smt2                           |  8 +++
 tests/str.at-3b.smt2                          |  9 ++++
 tests/str.at-3c.smt2                          | 15 ++++++
 8 files changed, 113 insertions(+), 4 deletions(-)
 create mode 100644 tests/str.at-3.smt2
 create mode 100644 tests/str.at-3b.smt2
 create mode 100644 tests/str.at-3c.smt2

diff --git a/src/main/scala/ostrich/BricsTransducer.scala b/src/main/scala/ostrich/BricsTransducer.scala
index 28685c7e37..b013bbdc67 100644
--- a/src/main/scala/ostrich/BricsTransducer.scala
+++ b/src/main/scala/ostrich/BricsTransducer.scala
@@ -90,6 +90,55 @@ object BricsTransducer {
         })
     }
 
+  /**
+   * Construct a transducer that extracts the <code>n</code>th-last character
+   * of a string.
+   */
+  def getStrAtRightTransducer(n : Int) : BricsTransducer =
+    synchronized {
+      strAtRightTransducer.getOrElseUpdate(
+        n, 
+        if (n < 0) {
+          SilentTransducer
+        } else {
+          import Transducer._
+
+          val builder = BricsTransducer.getBuilder
+
+          val initState      = builder.getNewState
+          val repeatState    = builder.getNewState
+          val tailStates     = for (i <- 0 to n)    yield builder.getNewState
+          val shortStrStates = for (i <- 1 until n) yield builder.getNewState
+
+          for (Seq(s1, s2) <- (tailStates sliding 2) ++
+                              ((List(initState) ++ shortStrStates) sliding 2) ++
+                              Iterator(List(repeatState, repeatState),
+                                       List(initState, repeatState)))
+            builder.addTransition(s1,
+                                  builder.LabelOps.sigmaLabel,
+                                  OutputOp("", NOP, ""),
+                                  s2)
+
+          builder.addTransition(initState,
+                                builder.LabelOps.sigmaLabel,
+                                OutputOp("", Plus(0), ""),
+                                tailStates.head)
+          builder.addTransition(repeatState,
+                                builder.LabelOps.sigmaLabel,
+                                OutputOp("", Plus(0), ""),
+                                tailStates.head)
+
+          builder.setInitialState(initState)
+          builder.setAccept(initState, true)
+          builder.setAccept(tailStates.last, true)
+
+          for (s <- shortStrStates)
+            builder.setAccept(s, true)
+
+          builder.getTransducer
+        })
+    }
+
   /**
    * Construct a transducer that removes the first <code>trimLeft</code>
    * and the last <code>trimRight</code> characters of a string.
@@ -148,7 +197,8 @@ object BricsTransducer {
     builder.getTransducer
   }
 
-  private val strAtTransducer = new MHashMap[Int, BricsTransducer]
+  private val strAtTransducer, strAtRightTransducer =
+    new MHashMap[Int, BricsTransducer]
 }
 
 class TransducerState extends BState {
diff --git a/src/main/scala/ostrich/OstrichPreprocessor.scala b/src/main/scala/ostrich/OstrichPreprocessor.scala
index a2c4a99e7c..f4980b5765 100644
--- a/src/main/scala/ostrich/OstrichPreprocessor.scala
+++ b/src/main/scala/ostrich/OstrichPreprocessor.scala
@@ -177,6 +177,14 @@ class OstrichPreprocessor(theory : OstrichStringTheory)
     case (IFunApp(`str_at`, _), Seq(bigStr : ITerm, Const(_))) =>
       t update subres
 
+    // keep str.at_last with concrete index, we will later translate it
+    // to a transducer
+    case (IFunApp(`str_at`, _),
+          Seq(bigStr : ITerm,
+              Difference(IFunApp(`str_len`, Seq(bigStr2)), Const(offset))))
+        if bigStr == bigStr2 && offset >= 1 =>
+      str_at_right(bigStr, offset - 1)
+
     case (IFunApp(`str_at`, _),
           Seq(bigStr : ITerm, index : ITerm)) => {
       val shBigStr3 = VariableShiftVisitor(bigStr, 0, 3)
diff --git a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
index 501df91eb8..44c09a7be5 100644
--- a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
+++ b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
@@ -44,7 +44,7 @@ import ap.basetypes.IdealInt
 class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
                                       facts : Conjunction) {
   import theory.{FunPred, strDatabase, autDatabase,
-                 str_++, str_at, str_trim,
+                 str_++, str_at, str_at_right, str_trim,
                  str_replaceall, str_replace,
                  str_replaceallre, str_replacere}
 
@@ -52,7 +52,8 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
 
   val translatablePredicates : Seq[Predicate] =
     (for (f <- List(str_++, str_replace, str_replaceall,
-                    str_replacere, str_replaceallre, str_at, str_trim) ++
+                    str_replacere, str_replaceallre,
+                    str_at, str_at_right, str_trim) ++
                theory.extraFunctionPreOps.keys)
      yield FunPred(f)) ++ theory.transducerPreOps.keys
   
@@ -97,6 +98,14 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
       }
       Some((op, List(a(0)), a(2)))
     }
+    case FunPred(`str_at_right`) => {
+      val op = () => {
+        val LinearCombination.Constant(IdealInt(ind)) = a(1)
+        // TODO: generate length information
+        TransducerPreOp(BricsTransducer.getStrAtRightTransducer(ind))
+      }
+      Some((op, List(a(0)), a(2)))
+    }
     case FunPred(`str_trim`) => {
       val op = () => {
         val LinearCombination.Constant(IdealInt(trimLeft))  = a(1)
diff --git a/src/main/scala/ostrich/OstrichStringTheory.scala b/src/main/scala/ostrich/OstrichStringTheory.scala
index 1188ffe7e5..bd3bec9a61 100644
--- a/src/main/scala/ostrich/OstrichStringTheory.scala
+++ b/src/main/scala/ostrich/OstrichStringTheory.scala
@@ -122,6 +122,9 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
     MonoSortedIFunction("re.from_ecma2020", List(SSo), RSo, true, false)
   val re_case_insensitive =
     MonoSortedIFunction("re.case_insensitive", List(RSo), RSo, true, false)
+  val str_at_right =
+    MonoSortedIFunction("str.at_right",
+                        List(SSo, Sort.Integer), SSo, true, false)
   val str_trim =
     MonoSortedIFunction("str.trim",
                         List(SSo, Sort.Integer, Sort.Integer), SSo, true, false)
@@ -152,6 +155,7 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
       yield (name, Right(p))) ++
      Iterator((re_from_ecma2020.name,    Left(re_from_ecma2020)),
               (re_case_insensitive.name, Left(re_case_insensitive)),
+              (str_at_right.name,        Left(str_at_right)),
               (str_trim.name,            Left(str_trim)))).toMap
 
   val extraIndexedOps : Map[(String, Int), Either[IFunction, Predicate]] = Map()
@@ -172,7 +176,7 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
   val functions =
     predefFunctions ++ List(str_empty, str_cons, str_head, str_tail) ++
     (extraStringFunctions map (_._2)) ++
-    List(re_from_ecma2020, re_case_insensitive, str_trim)
+    List(re_from_ecma2020, re_case_insensitive, str_at_right, str_trim)
 
   val (funPredicates, _, _, functionPredicateMap) =
     Theory.genAxioms(theoryFunctions = functions,
diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
index aa5dcf1bfc..13ae3866fa 100644
--- a/src/test/scala/SMTLIBTests.scala
+++ b/src/test/scala/SMTLIBTests.scala
@@ -196,6 +196,12 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
     checkFile("tests/str.at.smt2", "sat")
   property("str.at-2.smt2") =
     checkFile("tests/str.at-2.smt2", "unsat")
+  property("str.at-3.smt2") =
+    checkFile("tests/str.at-3.smt2", "sat")
+  property("str.at-3b.smt2") =
+    checkFile("tests/str.at-3b.smt2", "unsat")
+  property("str.at-3c.smt2") =
+    checkFile("tests/str.at-3c.smt2", "unsat")
   property("str.at-bug.smt2") =
     checkFile("tests/str.at-bug.smt2", "sat")
 
diff --git a/tests/str.at-3.smt2 b/tests/str.at-3.smt2
new file mode 100644
index 0000000000..49f8b127ff
--- /dev/null
+++ b/tests/str.at-3.smt2
@@ -0,0 +1,8 @@
+(set-logic QF_S)
+
+(declare-const x String)
+
+(assert (= (str.at x (- (str.len x) 1)) "x"))
+(assert (= (str.at x (- (str.len x) 2)) "y"))
+
+(check-sat)
diff --git a/tests/str.at-3b.smt2 b/tests/str.at-3b.smt2
new file mode 100644
index 0000000000..63a5c3425e
--- /dev/null
+++ b/tests/str.at-3b.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_S)
+
+(declare-const x String)
+
+(assert (= (str.at x (- (str.len x) 1)) "x"))
+(assert (= (str.at x (- (str.len x) 2)) "y"))
+(assert (< (str.len x) 2))
+
+(check-sat)
diff --git a/tests/str.at-3c.smt2 b/tests/str.at-3c.smt2
new file mode 100644
index 0000000000..a312888377
--- /dev/null
+++ b/tests/str.at-3c.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_S)
+
+(declare-const x String)
+
+(assert (not (and
+   (= (str.at "012" (- 1)) "")
+   (= (str.at "012" 0) "0")
+
+   (= (str.at "012" (- (str.len "012") 1)) "2")
+   (= (str.at "012" (- (str.len "012") 2)) "1")
+   (= (str.at "012" (- (str.len "012") 0)) "")
+   (distinct (str.at "000" (- (str.len "000") 5)) "0")
+)))
+
+(check-sat)

From fde80cfc8f5de84c6e44c190bc564d664455bfab Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Wed, 12 May 2021 14:15:57 +0200
Subject: [PATCH 10/27] add length information for some standard string
 functions

---
 src/main/scala/ostrich/AutomataUtils.scala    | 14 +++++++
 src/main/scala/ostrich/BricsAutomaton.scala   |  5 ++-
 src/main/scala/ostrich/Exploration.scala      | 17 +++++++-
 src/main/scala/ostrich/OFlags.scala           |  6 +++
 .../OstrichStringFunctionTranslator.scala     | 42 +++++++++++++++++--
 5 files changed, 77 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/ostrich/AutomataUtils.scala b/src/main/scala/ostrich/AutomataUtils.scala
index 2ed03083eb..ce9f71c563 100644
--- a/src/main/scala/ostrich/AutomataUtils.scala
+++ b/src/main/scala/ostrich/AutomataUtils.scala
@@ -222,6 +222,20 @@ object AutomataUtils {
                              yield aut.asInstanceOf[AtomicStateAutomaton],
                            len)
 
+  /**
+   * Product of a number of given automata
+   * The minimize argument enable minimization of the product automaton.
+   */
+  def product(auts : Seq[Automaton],
+              minimize : Boolean = false) : Automaton =
+    if (auts forall { _.isInstanceOf[AtomicStateAutomaton] }) {
+      productWithMap(auts map (_.asInstanceOf[AtomicStateAutomaton]),
+                     minimize)._1
+    } else {
+      // TODO: minimize?
+      auts reduceLeft (_ & _)
+    }
+
   /**
    * Product of a number of given automata.  Returns
    * new automaton.  Returns map from new states of result to (q0, [q1,
diff --git a/src/main/scala/ostrich/BricsAutomaton.scala b/src/main/scala/ostrich/BricsAutomaton.scala
index beccd8e355..f3ea580112 100644
--- a/src/main/scala/ostrich/BricsAutomaton.scala
+++ b/src/main/scala/ostrich/BricsAutomaton.scala
@@ -339,8 +339,11 @@ class BricsTLabelEnumerator(labels: Iterator[(Char, Char)])
 class BricsAutomaton(val underlying : BAutomaton) extends AtomicStateAutomaton {
 
   import BricsAutomaton.toBAutomaton
+  import OFlags.debug
 
-//  Console.err.println("Automata states: " + underlying.getNumberOfStates)
+  if (debug)
+    Console.err.println("New automaton with " + underlying.getNumberOfStates +
+                          " states")
 
   type State = BState
   type TLabel = (Char, Char)
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 23e4d044cf..2b8b4bf452 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -127,6 +127,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
                            flags : OFlags) {
 
   import Exploration._
+  import OFlags.debug
 
   def measure[A](op : String)(comp : => A) : A =
     if (flags.measureTimes)
@@ -331,6 +332,9 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
                       : ConflictSet = apps match {
 
     case List() => {
+      if (debug)
+        Console.err.println("Trying to contruct model")
+
       // we are finished and just have to construct a model
       val model = new MHashMap[Term, Either[IdealInt, Seq[Int]]]
 
@@ -403,9 +407,12 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
       }
       throw FoundModel(model.toMap)
     }
-    case (op, args, res) :: otherApps =>
+    case (op, args, res) :: otherApps => {
+      if (debug)
+        Console.err.println("dfExplore, depth " + apps.size)
       dfExploreOp(op, args, res, constraintStores(res).getContents,
                   otherApps)
+    }
   }
 
   private def dfExploreOp(op : PreOp,
@@ -418,6 +425,9 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
       dfExplore(nextApps)
 
     case resAut :: otherAuts => {
+      if (debug)
+        Console.err.println("dfExploreOp, #constraints " + resConstraints.size)
+
       ap.util.Timeout.check
 
       val argConstraints =
@@ -515,6 +525,8 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
   private def checkLengthConsistency : Option[Seq[TermConstraint]] =
     for (p <- lengthProver;
          if {
+           if (debug)
+             Console.err.println("checking length consistency")
            measure("check length consistency") {p.???} == ProverStatus.Unsat
          }) yield {
       for (n <- p.getUnsatCore.toList.sorted;
@@ -747,7 +759,8 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
     def getCompleteContents : List[Automaton] =
       constraints.toList
 
-    private def intersection : Automaton = constraints reduceLeft (_ & _)
+    private def intersection : Automaton =
+      AutomataUtils.product(constraints, _flags.minimizeAutomata)
 
     def ensureCompleteLengthConstraints : Unit =
       constraints match {
diff --git a/src/main/scala/ostrich/OFlags.scala b/src/main/scala/ostrich/OFlags.scala
index f46bab692b..128817ac33 100644
--- a/src/main/scala/ostrich/OFlags.scala
+++ b/src/main/scala/ostrich/OFlags.scala
@@ -38,6 +38,12 @@ object OFlags {
     val Off, On, Auto = Value
   }
 
+  /**
+   * Compile-time flag that can be used to switch on debugging output
+   * throughout the theory.
+   */
+  protected[ostrich] val debug = false
+
 }
 
 case class OFlags(
diff --git a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
index 44c09a7be5..0de5f94b98 100644
--- a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
+++ b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
@@ -32,7 +32,7 @@
 
 package ostrich
 
-import ap.terfor.Term
+import ap.terfor.{Term, Formula, TermOrder, TerForConvenience}
 import ap.terfor.conjunctions.Conjunction
 import ap.terfor.preds.{Atom, Predicate}
 import ap.terfor.linearcombination.LinearCombination
@@ -90,31 +90,65 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
       }
       Some((op, List(a(0), a(2)), a(3)))
     }
+
     case FunPred(`str_at`) => {
       val op = () => {
         val LinearCombination.Constant(IdealInt(ind)) = a(1)
         // TODO: generate length information
-        TransducerPreOp(BricsTransducer.getStrAtTransducer(ind))
+        new TransducerPreOp(BricsTransducer.getStrAtTransducer(ind)) {
+          override def toString = "str.at[" + ind + "]"
+          override def lengthApproximation(arguments : Seq[Term], result : Term,
+                                           order : TermOrder) : Formula = {
+            import TerForConvenience._
+            implicit val _ = order
+            result >= 0 & result <= 1 &
+            ((arguments(0)) <= ind <=> (result === 0))
+          }
+        }
       }
       Some((op, List(a(0)), a(2)))
     }
+
     case FunPred(`str_at_right`) => {
       val op = () => {
         val LinearCombination.Constant(IdealInt(ind)) = a(1)
         // TODO: generate length information
-        TransducerPreOp(BricsTransducer.getStrAtRightTransducer(ind))
+        new TransducerPreOp(BricsTransducer.getStrAtRightTransducer(ind)) {
+          override def toString = "str.at-right[" + ind + "]"
+          override def lengthApproximation(arguments : Seq[Term], result : Term,
+                                           order : TermOrder) : Formula = {
+            import TerForConvenience._
+            implicit val _ = order
+            result >= 0 & result <= 1 &
+            ((arguments(0)) <= ind <=> (result === 0))
+          }
+        }
       }
       Some((op, List(a(0)), a(2)))
     }
+
     case FunPred(`str_trim`) => {
       val op = () => {
         val LinearCombination.Constant(IdealInt(trimLeft))  = a(1)
         val LinearCombination.Constant(IdealInt(trimRight)) = a(2)
         // TODO: generate length information
-        TransducerPreOp(BricsTransducer.getTrimTransducer(trimLeft, trimRight))
+        new TransducerPreOp(BricsTransducer.getTrimTransducer(trimLeft,
+                                                              trimRight)) {
+          override def toString = "str.trim[" + trimLeft + ", " + trimRight +"]"
+          override def lengthApproximation(arguments : Seq[Term], result : Term,
+                                           order : TermOrder) : Formula = {
+            import TerForConvenience._
+            implicit val _ = order
+            ((arguments(0) >= trimLeft + trimRight) &
+               result === arguments(0) - (trimLeft + trimRight)) |
+            ((arguments(0) < trimLeft + trimRight) &
+               result === 0)
+          }
+        }
       }
       Some((op, List(a(0)), a(3)))
     }
+
     case FunPred(f) if theory.extraFunctionPreOps contains f => {
       val (op, argSelector, resSelector) = theory.extraFunctionPreOps(f)
       Some((() => op, argSelector(a), resSelector(a)))

From 989c7e6e265672f5966195d6a8cb26d3c888a5ef Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <ph_r@gmx.net>
Date: Wed, 12 May 2021 21:42:34 +0200
Subject: [PATCH 11/27] some experimental code

---
 .../scala/ostrich/OstrichPreprocessor.scala   | 47 +++++++++++++++++++
 1 file changed, 47 insertions(+)

diff --git a/src/main/scala/ostrich/OstrichPreprocessor.scala b/src/main/scala/ostrich/OstrichPreprocessor.scala
index f4980b5765..3272e3db32 100644
--- a/src/main/scala/ostrich/OstrichPreprocessor.scala
+++ b/src/main/scala/ostrich/OstrichPreprocessor.scala
@@ -155,6 +155,53 @@ class OstrichPreprocessor(theory : OstrichStringTheory)
           "")
  */
 
+/*
+    Some attempts to rewrite substr to replace; needs more thinking
+
+    case (IFunApp(`str_substr`, _),
+          Seq(bigStr : ITerm,
+              Const(IdealInt.ZERO),
+              IFunApp(`str_indexof`,
+                      Seq(bigStr2,
+                          ConcreteString(searchStr),
+                          Const(IdealInt.ZERO)))))
+        if bigStr == bigStr2 =>
+      ite(str_in_re(bigStr, reCat(re_all(), str_to_re(searchStr), re_all())),
+          str_replacere(bigStr, reCat(str_to_re(searchStr), re_all()), ""),
+          "")
+
+    case (IFunApp(`str_substr`, _),
+          Seq(bigStr : ITerm,
+              Const(IdealInt.ZERO),
+              Difference(IFunApp(`str_indexof`,
+                                 Seq(bigStr2,
+                                     ConcreteString(searchStr),
+                                     Const(IdealInt.ZERO))),
+                         Const(IdealInt(offset)))))
+        if bigStr == bigStr2 && (-offset) >= 1 && (-offset) <= searchStr.size =>
+      // TODO
+      ite(str_in_re(bigStr, reCat(re_all(), str_to_re(searchStr), re_all())),
+          str_replacere(bigStr,
+                        reCat(str_to_re(searchStr), re_all()),
+                        searchStr take (-offset)),
+          "")
+
+    case (IFunApp(`str_substr`, _),
+          Seq(bigStr : ITerm,
+              start@Difference(IFunApp(`str_indexof`,
+                                       Seq(bigStr2,
+                                           ConcreteString(searchStr),
+                                           Const(IdealInt.ZERO))),
+                               Const(IdealInt.MINUS_ONE)),
+              Difference(IFunApp(`str_len`, Seq(bigStr3)), start2)))
+        if bigStr == bigStr2 && bigStr == bigStr3 && searchStr.size == 1 &&
+           start == start2 =>
+      str_replacere(bigStr,
+                    reCat(re_*(re_comp(str_to_re(searchStr))),
+                          str_to_re(searchStr)),
+                    "")
+*/
+
     case (IFunApp(`str_substr`, _),
           Seq(bigStr : ITerm, begin : ITerm, len : ITerm)) => {
       val shBigStr3 = VariableShiftVisitor(bigStr, 0, 3)

From 7794cf717ecbe262c244d12bd117a17ccf132819 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <philipp.ruemmer@it.uu.se>
Date: Mon, 28 Jun 2021 14:14:08 +0200
Subject: [PATCH 12/27] Create scala.yml

---
 .github/workflows/scala.yml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)
 create mode 100644 .github/workflows/scala.yml

diff --git a/.github/workflows/scala.yml b/.github/workflows/scala.yml
new file mode 100644
index 0000000000..6814686602
--- /dev/null
+++ b/.github/workflows/scala.yml
@@ -0,0 +1,22 @@
+name: Scala CI
+
+on:
+  push:
+    branches: [ master ]
+  pull_request:
+    branches: [ master ]
+
+jobs:
+  build:
+
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v2
+    - name: Set up JDK 11
+      uses: actions/setup-java@v2
+      with:
+        java-version: '11'
+        distribution: 'adopt'
+    - name: Run tests
+      run: sbt test

From b7be8dc0c91907a555245a87ce20696375380c3d Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <philipp.ruemmer@it.uu.se>
Date: Mon, 28 Jun 2021 14:16:49 +0200
Subject: [PATCH 13/27] Delete build.properties

---
 project/build.properties | 1 -
 1 file changed, 1 deletion(-)
 delete mode 100644 project/build.properties

diff --git a/project/build.properties b/project/build.properties
deleted file mode 100644
index 6db9842501..0000000000
--- a/project/build.properties
+++ /dev/null
@@ -1 +0,0 @@
-sbt.version=1.4.0

From 02179c5db9cf25103197ea14ca6aa25c5b67f4d3 Mon Sep 17 00:00:00 2001
From: Philipp Ruemmer <philipp.ruemmer@it.uu.se>
Date: Mon, 28 Jun 2021 14:19:34 +0200
Subject: [PATCH 14/27] Update README.md

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index e0915a08f7..c97ddf4741 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-# OSTRICH [![Build Status](https://travis-ci.org/uuverifiers/ostrich.svg?branch=master)](https://travis-ci.org/uuverifiers/ostrich)
+# OSTRICH
 ## An SMT Solver for String Constraints
 
 OSTRICH is an SMT solver for string constraints.

From c33eb97c598ff3ca73b41488828203707deafc0f Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Fri, 19 Mar 2021 17:34:35 +0100
Subject: [PATCH 15/27] Base version (before upgrade)

---
 build.sbt                              |  16 ++-
 src/main/scala/ostrich/Automaton.scala | 165 +++----------------------
 2 files changed, 32 insertions(+), 149 deletions(-)

diff --git a/build.sbt b/build.sbt
index c9fb15c5b4..5046f46fca 100644
--- a/build.sbt
+++ b/build.sbt
@@ -5,13 +5,23 @@ lazy val commonSettings = Seq(
   scalaVersion := "2.11.12",
   crossScalaVersions := Seq("2.11.12", "2.12.10"),
   publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) ),
-  scalacOptions += "-deprecation",
+  scalacOptions ++= Seq(
+    "-deprecation",
+    //"-Xfatal-warnings",
+    "-unchecked",
+    "-Xlint",
+    "-Xelide-below", "FINE",
+    // "-feature",
+    // "-optimize",
+    "-Ywarn-dead-code",
+    "-Ywarn-unused"
+  ),
   resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/").withAllowInsecureProtocol(true),
   libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT",
   libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.5",
-  libraryDependencies += "org.sat4j" % "org.sat4j.core" % "2.3.1",
   libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.0" % "test",
-  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8"
+  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8",
+  libraryDependencies += "uuverifiers" %% "parikh-theory" % "0.1.0-SNAPSHOT"
 )
 
 lazy val root = (project in file(".")).
diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index e6912b7ea4..0363dc56fb 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -40,12 +40,20 @@ import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction}
 
 import scala.collection.mutable.{BitSet => MBitSet,
                                  HashMap => MHashMap, HashSet => MHashSet,
-                                 ArrayStack}
+  ArrayStack}
+
+import ap.parser.{IExpression, IFormula}
+import uuverifiers.parikh_theory.{
+  Automaton => OtherAutomaton,
+  LengthCounting
+}
+
 
 /**
  * Interface for different implementations of finite-state automata.
  */
 trait Automaton {
+
   /**
    * Union
    */
@@ -190,7 +198,7 @@ trait TLabelEnumerator[TLabel] {
  * don't have any structure and are not composite, there is a unique
  * initial state, and a set of accepting states.
  */
-trait AtomicStateAutomaton extends Automaton {
+trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   /**
    * Type of states
    */
@@ -201,6 +209,8 @@ trait AtomicStateAutomaton extends Automaton {
    */
   type TLabel
 
+  type Label = TLabel
+
   /**
    * Operations on labels
    */
@@ -257,9 +267,9 @@ trait AtomicStateAutomaton extends Automaton {
   /**
    * Iterate over all transitions
    */
-  def transitions : Iterator[(State, TLabel, State)] =
+  override def transitions : Iterator[(State, TLabel, State)] =
     for (s1 <- states.iterator; (s2, lbl) <- outgoingTransitions(s1))
-      yield (s1, lbl, s2)
+    yield (s1, lbl, s2)
 
   /**
    * Get image of a set of states under a given label
@@ -335,151 +345,14 @@ trait AtomicStateAutomaton extends Automaton {
   }
 
   /**
-   * Compute the length abstraction of this automaton. Special case of
-   * Parikh images, following the procedure in Verma et al, CADE 2005
-   */
-  lazy val getLengthAbstraction : Formula = /* Exploration.measure("length abstraction") */ {
+    * Compute the length abstraction of this automaton.
+    */
+  lazy val getLengthAbstraction: Formula = {
     import TerForConvenience._
     implicit val order = TermOrder.EMPTY
 
-    val stateSeq = states.toIndexedSeq
-    val state2Index = stateSeq.iterator.zipWithIndex.toMap
-
-    lazy val preStates = {
-      val preStates = Array.fill(stateSeq.size)(new MBitSet)
-
-      for ((from, _, to) <- transitions)
-        preStates(state2Index(to)) += state2Index(from)
-
-      preStates
-    }
-
-    lazy val transPreStates = {
-      val transPreStates = Array.fill(stateSeq.size)(new MBitSet)
-
-      for ((s1, s2) <- preStates.iterator zip transPreStates.iterator)
-        s2 ++= s1
-
-      for ((s, n) <- transPreStates.iterator.zipWithIndex)
-        s += n
-
-      // fixed-point iterator, to find transitively referenced states
-      var changed = true
-      while (changed) {
-        changed = false
-
-        for (i <- 0 until transPreStates.size) {
-          val set = transPreStates(i)
-
-          val oldSize = set.size
-          for (j <- 0 until transPreStates.size)
-            if (set contains j)
-              set |= transPreStates(j)
-
-          if (set.size > oldSize)
-            changed = true
-        }
-      }
-
-      transPreStates
-    }
-
-    val initialStateInd = state2Index(initialState)
-
-    ////////////////////////////////////////////////////////////////////////////
-
-    disjFor(for (finalState <- acceptingStates)
-            yield (uniqueLengthStates get finalState) match {
-
-    case Some(len) =>
-      v(0) === len
-
-    case None => {
-      val finalStateInd = state2Index(finalState)
-      val refStates = transPreStates(finalStateInd)
-
-      val productions : List[(Int, Option[Int])] =
-        (if (refStates contains initialStateInd)
-           List((initialStateInd, None))
-         else List()) :::
-        (for (state <- refStates.iterator;
-              preState <- preStates(state).iterator)
-         yield (state, Some(preState))).toList
-
-      val (prodVars, zVars, sizeVar) = {
-        val prodVars = for ((_, num) <- productions.zipWithIndex) yield v(num)
-        var nextVar = prodVars.size
-        val zVars = (for (state <- refStates.iterator) yield {
-          val ind = nextVar
-          nextVar = nextVar + 1
-          state -> v(ind)
-        }).toMap
-        (prodVars, zVars, v(nextVar))
-      }
-
-      // equations relating the production counters
-      val prodEqs =
-        (for (state <- refStates.iterator) yield {
-          LinearCombination(
-             (if (state == finalStateInd)
-                Iterator((IdealInt.ONE, OneTerm))
-              else
-                Iterator.empty) ++
-             (for (((source, targets), prodVar) <-
-                      productions.iterator zip prodVars.iterator;
-                    mult = (if (targets contains state) 1 else 0) -
-                           (if (source == state) 1 else 0))
-              yield (IdealInt(mult), prodVar)),
-             order)
-        }).toList
-
-      val sizeEq =
-        LinearCombination(
-          (for (((_, Some(_)), v) <- productions.iterator zip prodVars.iterator)
-           yield (IdealInt.ONE, v)) ++
-          Iterator((IdealInt.MINUS_ONE, sizeVar)),
-          order)
-
-      val entryZEq =
-        zVars(finalStateInd) - 1
-
-      val allEqs = eqZ(entryZEq :: sizeEq :: prodEqs)
-
-      val prodNonNeg =
-        prodVars >= 0
-
-      val prodImps =
-        (for (((source, _), prodVar) <-
-                productions.iterator zip prodVars.iterator;
-              if source != finalStateInd)
-         yield ((prodVar === 0) | (zVars(source) > 0))).toList
-
-      val zImps =
-        (for (state <- refStates.iterator; if state != finalStateInd) yield {
-           disjFor(Iterator(zVars(state) === 0) ++
-                   (for (((source, targets), prodVar) <-
-                           productions.iterator zip prodVars.iterator;
-                         if targets contains state)
-                    yield conj(zVars(state) === zVars(source) + 1,
-                               geqZ(List(prodVar - 1, zVars(source) - 1)))))
-         }).toList
-
-      val matrix =
-        conj(allEqs :: prodNonNeg :: prodImps ::: zImps)
-      val rawConstraint =
-        exists(prodVars.size + zVars.size, matrix)
-
-      val constraint =
-        ap.util.Timeout.withTimeoutMillis(1000) {
-          // best-effort attempt to get a quantifier-free version of the
-          // length abstraction
-          PresburgerTools.elimQuantifiersWithPreds(rawConstraint)
-        } {
-          ReduceWithConjunction(Conjunction.TRUE, order)(rawConstraint)
-        }
-
-      constraint
-    }})
+    val length = v(0)
+    (LengthCounting(IndexedSeq(this))) allowsMonoidValues Seq(length)
   }
 }
 

From f1185a1f323be0b74b004a9287ef600334420d89 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Mon, 22 Mar 2021 18:01:07 +0100
Subject: [PATCH 16/27] Port to scala 2.13 (with 24 warnings...)

---
 build.sbt                                     |  5 +--
 src/main/scala/ostrich/AutomataUtils.scala    | 22 +++++-----
 src/main/scala/ostrich/BricsAutomaton.scala   | 15 ++++---
 src/main/scala/ostrich/BricsTransducer.scala  | 16 ++++----
 src/main/scala/ostrich/CaleyGraph.scala       |  7 ++--
 src/main/scala/ostrich/ConcatPreOp.scala      |  5 +--
 src/main/scala/ostrich/ECMARegexParser.scala  | 41 ++++++++++---------
 src/main/scala/ostrich/Exploration.scala      | 27 ++++++------
 src/main/scala/ostrich/OstrichSolver.scala    |  5 +--
 .../ostrich/OstrichStringTheoryBuilder.scala  |  2 +-
 src/main/scala/ostrich/ReplaceAllPreOp.scala  |  2 +-
 src/main/scala/ostrich/TransducerPreOp.scala  |  1 -
 src/test/scala/APITest.scala                  |  4 +-
 .../ostrich/CaleyGraphSpecification.scala     |  7 +++-
 14 files changed, 76 insertions(+), 83 deletions(-)

diff --git a/build.sbt b/build.sbt
index 5046f46fca..bacaea16b6 100644
--- a/build.sbt
+++ b/build.sbt
@@ -2,8 +2,7 @@ lazy val commonSettings = Seq(
   name := "ostrich",
   organization := "uuverifiers",
   version := "1.0",
-  scalaVersion := "2.11.12",
-  crossScalaVersions := Seq("2.11.12", "2.12.10"),
+  scalaVersion := "2.13.5",
   publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) ),
   scalacOptions ++= Seq(
     "-deprecation",
@@ -30,5 +29,3 @@ lazy val root = (project in file(".")).
     mainClass in Compile := Some("ostrich.OstrichMain"),
     unmanagedSourceDirectories in Test += baseDirectory.value / "replaceall-benchmarks" / "src" / "test" / "scala"
   )
-
-
diff --git a/src/main/scala/ostrich/AutomataUtils.scala b/src/main/scala/ostrich/AutomataUtils.scala
index ce9f71c563..57edb57006 100644
--- a/src/main/scala/ostrich/AutomataUtils.scala
+++ b/src/main/scala/ostrich/AutomataUtils.scala
@@ -128,11 +128,11 @@ object AutomataUtils {
     consideredAuts += newAut
 
     // add automata until we encounter a conflict
-    var cont = areConsistentAutomata(consideredAuts)
+    var cont = areConsistentAutomata(consideredAuts.toSeq)
     val oldAutsIt = oldAuts.iterator
     while (cont && oldAutsIt.hasNext) {
       consideredAuts += oldAutsIt.next
-      cont = areConsistentAutomata(consideredAuts)
+      cont = areConsistentAutomata(consideredAuts.toSeq)
     }
 
     if (cont)
@@ -141,11 +141,11 @@ object AutomataUtils {
     // remove automata to get a small core
     for (i <- (consideredAuts.size - 2) to 1 by -1) {
       val removedAut = consideredAuts remove i
-      if (areConsistentAutomata(consideredAuts))
+      if (areConsistentAutomata(consideredAuts.toSeq))
         consideredAuts.insert(i, removedAut)
     }
 
-    Some(consideredAuts)
+    Some(consideredAuts.toSeq)
   }
 
   /**
@@ -205,7 +205,7 @@ object AutomataUtils {
           if (isAccepting(reached) && wSize + 1 == len)
             return Some(newW.reverse)
           if (wSize + 1 < len)
-            todo push (reached, newW)
+            todo push ((reached, newW))
         }
     }
 
@@ -399,7 +399,7 @@ object AutomataUtils {
         states : Iterable[(A#State, A#State)]) : AtomicStateAutomaton = {
     val builder = aut.getBuilder
     val smap : Map[A#State, aut.State] =
-      aut.states.map(s => (s -> builder.getNewState))(collection.breakOut)
+      aut.states.iterator.map(s => (s -> builder.getNewState)).toMap
 
     for ((s1, lbl, s2) <- aut.transitions)
       for (newLbl <- aut.LabelOps.subtractLetter(a, lbl))
@@ -424,7 +424,7 @@ object AutomataUtils {
     val builder = aut.getBuilder
 
     val smap : Map[aut.State, aut.State] =
-      aut.states.map(s => (s -> builder.getNewState))(collection.breakOut)
+      aut.states.iterator.map(s => (s -> builder.getNewState)).toMap
 
     val initState = builder.initialState
     builder.setAccept(smap(aut.initialState), true)
@@ -448,9 +448,9 @@ object AutomataUtils {
     val builder = aut1.getBuilder
 
     val smap1 : Map[aut1.State, aut1.State] =
-      aut1.states.map(s => (s -> builder.getNewState))(collection.breakOut)
+      aut1.states.iterator.map(s => (s -> builder.getNewState)).toMap
     val smap2 : Map[aut2.State, aut1.State] =
-      aut2.states.map(s => (s -> builder.getNewState))(collection.breakOut)
+      aut2.states.iterator.map(s => (s -> builder.getNewState)).toMap
 
     builder.setInitialState(smap1(aut1.initialState))
     for (sf <- aut2.acceptingStates)
@@ -490,9 +490,9 @@ object AutomataUtils {
     val builder = autOuter.getBuilder
 
     val smapOuter : Map[autOuter.State, autOuter.State] =
-      autOuter.states.map(s => (s -> builder.getNewState))(collection.breakOut)
+      autOuter.states.iterator.map(s => (s -> builder.getNewState)).toMap
     val smapInner : Map[autInner.State, autOuter.State] =
-      autInner.states.map(s => (s -> builder.getNewState))(collection.breakOut)
+      autInner.states.iterator.map(s => (s -> builder.getNewState)).toMap
 
     val innerInit = smapInner(autInner.initialState)
     val innerFinal = autInner.acceptingStates.map(smapInner)
diff --git a/src/main/scala/ostrich/BricsAutomaton.scala b/src/main/scala/ostrich/BricsAutomaton.scala
index f3ea580112..9799ef42ea 100644
--- a/src/main/scala/ostrich/BricsAutomaton.scala
+++ b/src/main/scala/ostrich/BricsAutomaton.scala
@@ -35,8 +35,6 @@ package ostrich
 import dk.brics.automaton.{BasicAutomata, BasicOperations, RegExp, Transition,
                            Automaton => BAutomaton, State => BState}
 
-import scala.collection.JavaConversions.{asScalaIterator,
-                                         iterableAsScalaIterable}
 import scala.collection.mutable.{HashMap => MHashMap,
                                  HashSet => MHashSet,
                                  LinkedHashSet => MLinkedHashSet,
@@ -44,6 +42,7 @@ import scala.collection.mutable.{HashMap => MHashMap,
                                  TreeSet => MTreeSet,
                                  MultiMap => MMultiMap,
                                  Set => MSet}
+import scala.jdk.CollectionConverters._
 
 object BricsAutomaton {
   private def toBAutomaton(aut : Automaton) : BAutomaton = aut match {
@@ -253,8 +252,8 @@ class BricsTLabelEnumerator(labels: Iterator[(Char, Char)])
   def enumLabelOverlap(lbl : (Char, Char)) : Iterable[(Char, Char)] = {
     val (lMin, lMax) = lbl
     disjointLabels.
-      from((lMin, Char.MinValue)).
-      to((lMax, Char.MaxValue)).
+      rangeFrom((lMin, Char.MinValue)).
+      rangeTo((lMax, Char.MaxValue)).
       toIterable
   }
 
@@ -425,7 +424,7 @@ class BricsAutomaton(val underlying : BAutomaton) extends AtomicStateAutomaton {
   def outgoingTransitions(from : State) : Iterator[(State, TLabel)] = {
     val dests = new MHashMap[TLabel, MSet[State]] with MMultiMap[TLabel, State]
 
-    for (t <- from.getTransitions)
+    for (t <- from.getTransitions.asScala)
       dests.addBinding((t.getMin, t.getMax), t.getDest)
 
     val outgoing = new MLinkedHashSet[(State, TLabel)]
@@ -434,9 +433,9 @@ class BricsAutomaton(val underlying : BAutomaton) extends AtomicStateAutomaton {
 
       def sortingFn(s1 : State, s2 : State) : Boolean = {
         // sort by lowest outgoing transition
-        for ((t1, t2) <- s1.getSortedTransitions(false)
+        for ((t1, t2) <- s1.getSortedTransitions(false).asScala
                          zip
-                         s2.getSortedTransitions(false)) {
+                         s2.getSortedTransitions(false).asScala) {
           import scala.math.Ordering.Implicits._
           val lbl1 = (t1.getMin, t1.getMax)
           val lbl2 = (t2.getMin, t2.getMax)
@@ -540,7 +539,7 @@ class BricsAutomatonBuilder
 
   def outgoingTransitions(q : BricsAutomaton#State)
         : Iterator[(BricsAutomaton#State, BricsAutomaton#TLabel)] =
-    for (t <- q.getTransitions.iterator)
+    for (t <- q.getTransitions.asScala.iterator)
       yield (t.getDest, (t.getMin, t.getMax))
 
   def setAccept(q : BricsAutomaton#State, isAccepting : Boolean) : Unit =
diff --git a/src/main/scala/ostrich/BricsTransducer.scala b/src/main/scala/ostrich/BricsTransducer.scala
index b013bbdc67..502bb91e36 100644
--- a/src/main/scala/ostrich/BricsTransducer.scala
+++ b/src/main/scala/ostrich/BricsTransducer.scala
@@ -43,9 +43,9 @@ import dk.brics.automaton.{Automaton => BAutomaton,
                            State => BState,
                            Transition => BTransition}
 
-import scala.collection.JavaConversions.{iterableAsScalaIterable,asJavaCollection}
 
 import java.lang.StringBuilder
+import scala.collection.MapView
 
 object BricsTransducer {
   def apply() : BricsTransducer =
@@ -212,9 +212,9 @@ class TransducerState extends BState {
  * a character of output
  */
 class BricsTransducer(val initialState : BricsAutomaton#State,
-                      val lblTrans: Map[BricsAutomaton#State,
+                      val lblTrans: MapView[BricsAutomaton#State,
                                         Set[BricsTransducer#TTransition]],
-                      val eTrans: Map[BricsAutomaton#State,
+                      val eTrans: MapView[BricsAutomaton#State,
                                       Set[BricsTransducer#TETransition]],
                       val acceptingStates : Set[BricsAutomaton#State])
     extends Transducer {
@@ -816,11 +816,11 @@ class BricsTransducerBuilder
           worklist.push(snext)
     }
 
-    acceptingStates.retain(bwdReach.contains(_))
-    lblTrans.retain((k, v) => bwdReach.contains(k))
-    eTrans.retain((k, v) => bwdReach.contains(k))
-    lblTrans.foreach({ case (k, v) => v.retain(t => bwdReach.contains(dest(t))) })
-    eTrans.foreach({ case (k, v) => v.retain(t => bwdReach.contains(edest(t))) })
+    acceptingStates.filterInPlace(bwdReach.contains(_))
+    lblTrans.filterInPlace{case (k, v) => bwdReach.contains(k)}
+    eTrans.filterInPlace{case (k, v) => bwdReach.contains(k)}
+    lblTrans.foreach({ case (k, v) => v.filterInPlace(t => bwdReach.contains(dest(t))) })
+    eTrans.foreach({ case (k, v) => v.filterInPlace(t => bwdReach.contains(edest(t))) })
   }
 }
 
diff --git a/src/main/scala/ostrich/CaleyGraph.scala b/src/main/scala/ostrich/CaleyGraph.scala
index 8104a97eac..747eed6c96 100644
--- a/src/main/scala/ostrich/CaleyGraph.scala
+++ b/src/main/scala/ostrich/CaleyGraph.scala
@@ -35,8 +35,7 @@ package ostrich
 import java.util.Objects
 
 import scala.collection.mutable.{HashMap, HashSet, Set, Stack, MultiMap}
-import scala.collection.JavaConversions._
-import scala.collection.IterableView
+import scala.collection.MapView
 
 object Box {
   /**
@@ -171,10 +170,10 @@ object CaleyGraph {
   }
 
   private def getCharacterBoxes[A <: AtomicStateAutomaton](aut : A)
-      : Map[Box[A], Iterable[A#TLabel]] = {
+      : MapView[Box[A], Iterable[A#TLabel]] = {
     val ae = aut.labelEnumerator
     val boxes : Map[A#TLabel,Box[A]] =
-      ae.enumDisjointLabels.map(i => i -> new Box[A])(collection.breakOut)
+      ae.enumDisjointLabels.iterator.map(i => i -> new Box[A]).toMap
 
     for ((q1, i, q2) <- aut.transitions;
          i2 <- ae.enumLabelOverlap(i))
diff --git a/src/main/scala/ostrich/ConcatPreOp.scala b/src/main/scala/ostrich/ConcatPreOp.scala
index 9496574acf..43bc58c22f 100644
--- a/src/main/scala/ostrich/ConcatPreOp.scala
+++ b/src/main/scala/ostrich/ConcatPreOp.scala
@@ -34,9 +34,6 @@ package ostrich
 
 import ap.terfor.{Term, Formula, TermOrder, TerForConvenience}
 
-import scala.collection.JavaConversions.{asScalaIterator,
-                                         iterableAsScalaIterable}
-
 /**
  * Pre-image computation for the concatenation operator.
  */
@@ -113,7 +110,7 @@ object ConcatPreOp extends PreOp {
   override def lengthApproximation(arguments : Seq[Term], result : Term,
                                    order : TermOrder) : Formula = {
     import TerForConvenience._
-    implicit val _ = order
+    implicit val o = order
     result === arguments(0) + arguments(1)
   }
 
diff --git a/src/main/scala/ostrich/ECMARegexParser.scala b/src/main/scala/ostrich/ECMARegexParser.scala
index 8970e30067..b6aa21f9ff 100644
--- a/src/main/scala/ostrich/ECMARegexParser.scala
+++ b/src/main/scala/ostrich/ECMARegexParser.scala
@@ -39,7 +39,8 @@ import ecma2020regex._
 import ecma2020regex.Absyn._
 import ecma2020regex.Absyn.{Quantifier => ECMAQuantifier}
 
-import scala.collection.JavaConversions.{asScalaBuffer, asScalaIterator}
+// import scala.collection.JavaConverters._
+import scala.jdk.CollectionConverters._
 
 object ECMARegexParser {
 
@@ -104,11 +105,11 @@ class ECMARegexParser(theory : OstrichStringTheory) {
     def combine(x : ITerm, y : ITerm, arg : VisitorArg) : ITerm = reCat(x, y)
 
     override def visit(p : ecma2020regex.Absyn.Pattern, arg : VisitorArg) =
-      reUnionStar(p.listalternativec_ map (_.accept(this, arg)) : _*)
+      reUnionStar(p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*)
 
     override def visit(p : ecma2020regex.Absyn.Alternative,
                        outermost : VisitorArg) = {
-      val terms = expandGroups(p.listtermc_) map (_.accept(this, false))
+      val terms = expandGroups(p.listtermc_.asScala.toSeq) map (_.accept(this, false))
 
       if (outermost) {
         // handle leading look-aheads and trailing look-behinds
@@ -163,12 +164,12 @@ class ECMARegexParser(theory : OstrichStringTheory) {
                  case g : ecma2020regex.Absyn.GroupAtom
                      if g.listalternativec_.size == 1 => {
                        changed = true
-                       altToTerms(g.listalternativec_)
+                       altToTerms(g.listalternativec_.asScala.toSeq)
                      }
                  case g : ecma2020regex.Absyn.NonCaptGroup
                      if g.listalternativec_.size == 1 => {
                        changed = true
-                       altToTerms(g.listalternativec_)
+                       altToTerms(g.listalternativec_.asScala.toSeq)
                      }
                  case _ =>
                    List(t)
@@ -185,7 +186,7 @@ class ECMARegexParser(theory : OstrichStringTheory) {
                          : Seq[ecma2020regex.Absyn.TermC] = {
       assert(a.size == 1)
       val alt = a.head.asInstanceOf[ecma2020regex.Absyn.Alternative]
-      alt.listtermc_.toList
+      alt.listtermc_.asScala.toList
     }
 
     private def dropAssertions(ts : Seq[ITerm]) : Seq[ITerm] =
@@ -212,31 +213,31 @@ class ECMARegexParser(theory : OstrichStringTheory) {
 
     override def visit(p : ecma2020regex.Absyn.GroupAtom, arg : VisitorArg) =
       // capture group
-      reUnionStar(p.listalternativec_ map (_.accept(this, arg)) : _*)
+      reUnionStar(p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*)
     override def visit(p : ecma2020regex.Absyn.NonCaptGroup, arg : VisitorArg) =
       // non-capture group
-      reUnionStar(p.listalternativec_ map (_.accept(this, arg)) : _*)
+      reUnionStar(p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*)
 
     override def visit(p : ecma2020regex.Absyn.PosLookahead, arg : VisitorArg) =
       LookAhead(
-        reCat(reUnionStar(p.listalternativec_ map (_.accept(this, arg)) : _*),
+        reCat(reUnionStar(p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*),
               ALL))
     override def visit(p : ecma2020regex.Absyn.NegLookahead, arg : VisitorArg) =
       LookAhead(
         re_comp(reCat(reUnionStar(
-          p.listalternativec_ map (_.accept(this, arg)) : _*), ALL)))
+          p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*), ALL)))
 
     override def visit(p : ecma2020regex.Absyn.PosLookbehind,
                        arg : VisitorArg) =
       LookBehind(
         reCat(ALL, reUnionStar(
-                p.listalternativec_ map (_.accept(this, arg)) : _*)))
+                p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*)))
 
     override def visit(p : ecma2020regex.Absyn.NegLookbehind,
                        arg : VisitorArg) =
       LookBehind(
         re_comp(reCat(ALL, reUnionStar(
-                  p.listalternativec_ map (_.accept(this, arg)) : _*))))
+                  p.listalternativec_.asScala.toSeq map (_.accept(this, arg)) : _*))))
 
     override def visit(p : ecma2020regex.Absyn.DotAtom, arg : VisitorArg) =
       charComplement(lineTerminator) // . is anything apart from a line term.
@@ -277,16 +278,16 @@ class ECMARegexParser(theory : OstrichStringTheory) {
         case _ : PlusQuantifier  => re_+(t)
         case _ : OptQuantifier   => re_opt(t)
         case q : Loop1Quantifier => {
-          val n = parseDecimalDigits(q.listdecimaldigit_)
+          val n = parseDecimalDigits(q.listdecimaldigit_.asScala.toSeq)
           re_loop(n, n, t)
         }
         case q : Loop2Quantifier => {
-          val n = parseDecimalDigits(q.listdecimaldigit_)
+          val n = parseDecimalDigits(q.listdecimaldigit_.asScala.toSeq)
           reCat(re_loop(n, n, t), re_*(t))
         }
         case q : Loop3Quantifier => {
-          val n1 = parseDecimalDigits(q.listdecimaldigit_1)
-          val n2 = parseDecimalDigits(q.listdecimaldigit_2)
+          val n1 = parseDecimalDigits(q.listdecimaldigit_1.asScala.toSeq)
+          val n2 = parseDecimalDigits(q.listdecimaldigit_2.asScala.toSeq)
           re_loop(n1, n2, t)
         }
       }
@@ -420,7 +421,7 @@ class ECMARegexParser(theory : OstrichStringTheory) {
         p.maybedecimaldigits_ match {
           case _ : NoDecimalDigits => ""
           case ds : SomeDecimalDigits =>
-            (for (d <- ds.listdecimaldigit_)
+            (for (d <- ListHasAsScala(ds.listdecimaldigit_).asScala)
              yield (printer print d)).mkString("")
         }
       val allDigits =
@@ -519,7 +520,7 @@ class ECMARegexParser(theory : OstrichStringTheory) {
     case (x,     y    ) => re_++(x, y)
   }
 
-  private def reCatStar(xs : ITerm*) = (EPS /: xs) (reCat _)
+  private def reCatStar(xs : ITerm*) = xs.foldLeft(EPS) (reCat _)
 
   private def reUnion(x : ITerm, y : ITerm) = (x, y) match {
     case (`NONE`, y    ) => y
@@ -527,7 +528,7 @@ class ECMARegexParser(theory : OstrichStringTheory) {
     case (x,     y     ) => re_union(x, y)
   }
 
-  private def reUnionStar(xs : ITerm*) = (NONE /: xs) (reUnion _)
+  private def reUnionStar(xs : ITerm*) = xs.foldLeft(NONE) (reUnion _)
 
   private def reInter(x : ITerm, y : ITerm) = (x, y) match {
     case (`ALL`, y    ) => y
@@ -535,7 +536,7 @@ class ECMARegexParser(theory : OstrichStringTheory) {
     case (x,     y    ) => re_inter(x, y)
   }
 
-  private def reInterStar(xs : ITerm*) = (ALL /: xs) (reInter _)
+  private def reInterStar(xs : ITerm*) = xs.foldLeft(ALL) (reInter _)
 
   private lazy val decimal =
     re_charrange(48, 57)
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 2b8b4bf452..6cf2a5e5ab 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -40,7 +40,6 @@ import ap.terfor.linearcombination.LinearCombination
 import ap.terfor.substitutions.VariableSubst
 import ap.util.Seqs
 
-import scala.collection.breakOut
 import scala.collection.mutable.{HashMap => MHashMap, ArrayBuffer, ArrayStack,
                                  HashSet => MHashSet, LinkedHashSet,
                                  BitSet => MBitSet}
@@ -222,7 +221,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
     // check whether any of the terms have concrete definitions
     for (t <- allTerms)
       for (w <- strDatabase.term2List(t)) {
-        val str : String = w.map(i => i.toChar)(breakOut)
+        val str = w.iterator.map(i => i.toChar).mkString
         additionalConstraints += ((t, BricsAutomaton fromString str))
         for (ind <- term2Index get t)
           coveredTerms += ind
@@ -399,7 +398,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
             throw new Exception(
               "Could not satisfy length constraints for " + res +
                 " with solution " +
-                resValue.right.get.map(i => i.toChar)(breakOut) +
+                resValue.right.get.iterator.map(i => i.toChar).mkString +
                 "; length is " + resValue.right.get.size +
                 " but should be " + resLen)
 
@@ -544,7 +543,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
   private def popLengthConstraints : Unit =
     for (p <- lengthProver) {
       p.pop
-      lengthPartitions reduceToSize lengthPartitionStack.pop
+      lengthPartitions dropRightInPlace (lengthPartitions.size - lengthPartitionStack.pop())
     }
 
   //////////////////////////////////////////////////////////////////////////////
@@ -580,11 +579,11 @@ class EagerExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
     private val constraintStack = new ArrayStack[(Int, Option[Automaton])]
 
     def push : Unit =
-      constraintStack push (constraints.size, currentConstraint)
+      constraintStack push((constraints.size, currentConstraint))
 
     def pop : Unit = {
-      val (oldSize, lastCC) = constraintStack.pop
-      constraints reduceToSize oldSize
+      val (oldSize, lastCC) = constraintStack.pop()
+      constraints dropRightInPlace (constraints.size - oldSize)
       currentConstraint = lastCC
     }
 
@@ -602,7 +601,7 @@ class EagerExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
               constraints += aut
               currentConstraint = Some(newAut)
               addLengthConstraint(TermConstraint(t, newAut),
-                                  for (a <- constraints)
+                                  for (a <- constraints.toSeq)
                                   yield TermConstraint(t, a))
               None
             }
@@ -703,10 +702,10 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
     def push : Unit = constraintStack push constraints.size
 
     def pop : Unit = {
-      val oldSize = constraintStack.pop
+      val oldSize = constraintStack.pop()
       while (constraints.size > oldSize) {
         constraintSet -= constraints.last
-        constraints reduceToSize (constraints.size - 1)
+        constraints dropRightInPlace (1)
       }
     }
 
@@ -739,7 +738,7 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
           potentialConflicts = potentialConflicts.tail
         }
 
-        measure("AutomataUtils.findUnsatCore") { AutomataUtils.findUnsatCore(constraints, aut) } match {
+        measure("AutomataUtils.findUnsatCore") { AutomataUtils.findUnsatCore(constraints.toSeq, aut) } match {
           case Some(core) => {
             addIncAutomata(core)
             Some(for (a <- core.toList) yield TermConstraint(t, a))
@@ -768,20 +767,20 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
           // nothing, all length constraints already pushed
         case auts =>
           addLengthConstraint(TermConstraint(t, intersection),
-                              for (a <- constraints)
+                              for (a <- constraints.toSeq)
                               yield TermConstraint(t, a))
       }
 
     def getAcceptedWord : Seq[Int] =
       constraints match {
         case Seq() => List()
-        case auts  => intersection.getAcceptedWord.get
+        case auts  => intersection.getAcceptedWord.get.toSeq
       }
 
     def getAcceptedWordLen(len : Int) : Seq[Int] =
       constraints match {
         case Seq() => for (_ <- 0 until len) yield 0
-        case auts  => AutomataUtils.findAcceptedWord(auts, len).get
+        case auts  => AutomataUtils.findAcceptedWord(auts.toSeq, len).get
       }
   }
 
diff --git a/src/main/scala/ostrich/OstrichSolver.scala b/src/main/scala/ostrich/OstrichSolver.scala
index 4b93c46b68..7bbb8a429b 100644
--- a/src/main/scala/ostrich/OstrichSolver.scala
+++ b/src/main/scala/ostrich/OstrichSolver.scala
@@ -43,7 +43,6 @@ import ap.basetypes.IdealInt
 
 import dk.brics.automaton.{RegExp, Automaton => BAutomaton}
 
-import scala.collection.breakOut
 import scala.collection.mutable.{ArrayBuffer, HashMap => MHashMap}
 
 class OstrichSolver(theory : OstrichStringTheory,
@@ -253,10 +252,10 @@ class OstrichSolver(theory : OstrichStringTheory,
 
       val exploration =
         if (eagerMode)
-          Exploration.eagerExp(funApps, regexes, strDatabase,
+          Exploration.eagerExp(funApps.toSeq, regexes.toSeq, strDatabase,
                                lProver, lengthVars.toMap, useLength, flags)
         else
-          Exploration.lazyExp(funApps, regexes, strDatabase,
+          Exploration.lazyExp(funApps.toSeq, regexes.toSeq, strDatabase,
                               lProver, lengthVars.toMap, useLength, flags)
 
       exploration.findModel
diff --git a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
index 20788364d0..ba13e90168 100644
--- a/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
+++ b/src/main/scala/ostrich/OstrichStringTheoryBuilder.scala
@@ -103,7 +103,7 @@ class OstrichStringTheoryBuilder extends StringTheoryBuilder {
         (name, aut)
       }
 
-    new OstrichStringTheory (symTransducers,
+    new OstrichStringTheory (symTransducers.toSeq,
                              OFlags(eagerAutomataOperations = eager,
                                     useLength               = useLen,
                                     forwardApprox           = forward,
diff --git a/src/main/scala/ostrich/ReplaceAllPreOp.scala b/src/main/scala/ostrich/ReplaceAllPreOp.scala
index d5ab04ea93..42253be4a1 100644
--- a/src/main/scala/ostrich/ReplaceAllPreOp.scala
+++ b/src/main/scala/ostrich/ReplaceAllPreOp.scala
@@ -87,7 +87,7 @@ class ReplaceAllPreOpChar(a : Char) extends PreOp {
   override def lengthApproximation(arguments : Seq[Term], result : Term,
                                    order : TermOrder) : Formula = {
     import TerForConvenience._
-    implicit val _ = order
+    implicit val o = order
     (arguments(1) === 1 & result === arguments(0)) |
     (arguments(1) < 1 & result <= arguments(0)) |
     (arguments(1) > 1 & result >= arguments(0))
diff --git a/src/main/scala/ostrich/TransducerPreOp.scala b/src/main/scala/ostrich/TransducerPreOp.scala
index 6cffd75ef6..f5ead235f8 100644
--- a/src/main/scala/ostrich/TransducerPreOp.scala
+++ b/src/main/scala/ostrich/TransducerPreOp.scala
@@ -32,7 +32,6 @@
 
 package ostrich
 
-import scala.collection.breakOut
 
 object TransducerPreOp {
   def apply(t : Transducer) = new TransducerPreOp(t)
diff --git a/src/test/scala/APITest.scala b/src/test/scala/APITest.scala
index c946ce6457..f738c1eda6 100644
--- a/src/test/scala/APITest.scala
+++ b/src/test/scala/APITest.scala
@@ -28,7 +28,7 @@ object APITest extends Properties("APITest") {
       import p._
 
       val x, y, z = createConstant(StringSort)
-      implicit val _ = decoderContext
+      implicit val context = decoderContext
 
       scope {
         !! (x === "abc")
@@ -62,7 +62,7 @@ object APITest extends Properties("APITest") {
       import p._
 
       val x, y, z = createConstant(StringSort)
-      implicit val _ = decoderContext
+      implicit val context = decoderContext
 
       scope {
         !! (x ++ y === y ++ x)
diff --git a/src/test/scala/ostrich/CaleyGraphSpecification.scala b/src/test/scala/ostrich/CaleyGraphSpecification.scala
index b0b3a71307..a468633e15 100644
--- a/src/test/scala/ostrich/CaleyGraphSpecification.scala
+++ b/src/test/scala/ostrich/CaleyGraphSpecification.scala
@@ -4,15 +4,18 @@ import org.scalacheck.{Arbitrary, Gen, Properties}
 import org.scalacheck.Prop._
 import dk.brics.automaton.{Automaton => BAutomaton, State, Transition}
 import scala.collection.mutable.Set
-import scala.collection.JavaConversions.iterableAsScalaIterable
+
+
+import scala.jdk.CollectionConverters._
 
 class PrintableState extends State {
   override def toString = "q" + hashCode
 }
 
 class IDState(val ident : Int) extends State {
+
   override def toString =
-    getTransitions.foldLeft("q" + ident + '\n') { (s, t) =>
+    getTransitions.asScala.foldLeft("q" + ident + '\n') { (s, t) =>
       val dest = t.getDest match {
         case d : IDState => "q" + d.ident
         case q => q.toString

From 0891558d3daffbacdac7954a5bbcb1d8c606fb0d Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Tue, 23 Mar 2021 12:24:52 +0100
Subject: [PATCH 17/27] Roll back the use of the Parikh theory. This is now a
 clean 2.13 port.

---
 build.sbt                              |   3 +-
 src/main/scala/ostrich/Automaton.scala | 160 ++++++++++++++++++++++---
 src/test/scala/SMTLIBTests.scala       |   2 +-
 3 files changed, 147 insertions(+), 18 deletions(-)

diff --git a/build.sbt b/build.sbt
index bacaea16b6..c1fa0d95e6 100644
--- a/build.sbt
+++ b/build.sbt
@@ -19,8 +19,7 @@ lazy val commonSettings = Seq(
   libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT",
   libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.5",
   libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.0" % "test",
-  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8",
-  libraryDependencies += "uuverifiers" %% "parikh-theory" % "0.1.0-SNAPSHOT"
+  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8"
 )
 
 lazy val root = (project in file(".")).
diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index 0363dc56fb..5e6fab762e 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -34,7 +34,7 @@ package ostrich
 
 import ap.basetypes.IdealInt
 import ap.PresburgerTools
-import ap.terfor.{Formula, Term, TerForConvenience, TermOrder, OneTerm}
+import ap.terfor.{Formula, TerForConvenience, TermOrder, OneTerm}
 import ap.terfor.linearcombination.LinearCombination
 import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction}
 
@@ -42,13 +42,6 @@ import scala.collection.mutable.{BitSet => MBitSet,
                                  HashMap => MHashMap, HashSet => MHashSet,
   ArrayStack}
 
-import ap.parser.{IExpression, IFormula}
-import uuverifiers.parikh_theory.{
-  Automaton => OtherAutomaton,
-  LengthCounting
-}
-
-
 /**
  * Interface for different implementations of finite-state automata.
  */
@@ -198,7 +191,7 @@ trait TLabelEnumerator[TLabel] {
  * don't have any structure and are not composite, there is a unique
  * initial state, and a set of accepting states.
  */
-trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
+trait AtomicStateAutomaton extends Automaton  {
   /**
    * Type of states
    */
@@ -267,7 +260,7 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   /**
    * Iterate over all transitions
    */
-  override def transitions : Iterator[(State, TLabel, State)] =
+  def transitions : Iterator[(State, TLabel, State)] =
     for (s1 <- states.iterator; (s2, lbl) <- outgoingTransitions(s1))
     yield (s1, lbl, s2)
 
@@ -345,14 +338,151 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   }
 
   /**
-    * Compute the length abstraction of this automaton.
-    */
-  lazy val getLengthAbstraction: Formula = {
+   * Compute the length abstraction of this automaton. Special case of
+   * Parikh images, following the procedure in Verma et al, CADE 2005
+   */
+   lazy val getLengthAbstraction : Formula = /* Exploration.measure("length abstraction") */ {
     import TerForConvenience._
     implicit val order = TermOrder.EMPTY
 
-    val length = v(0)
-    (LengthCounting(IndexedSeq(this))) allowsMonoidValues Seq(length)
+    val stateSeq = states.toIndexedSeq
+    val state2Index = stateSeq.iterator.zipWithIndex.toMap
+
+    lazy val preStates = {
+      val preStates = Array.fill(stateSeq.size)(new MBitSet)
+
+      for ((from, _, to) <- transitions)
+        preStates(state2Index(to)) += state2Index(from)
+
+      preStates
+    }
+
+    lazy val transPreStates = {
+      val transPreStates = Array.fill(stateSeq.size)(new MBitSet)
+
+      for ((s1, s2) <- preStates.iterator zip transPreStates.iterator)
+        s2 ++= s1
+
+      for ((s, n) <- transPreStates.iterator.zipWithIndex)
+        s += n
+
+      // fixed-point iterator, to find transitively referenced states
+      var changed = true
+      while (changed) {
+        changed = false
+
+        for (i <- 0 until transPreStates.size) {
+          val set = transPreStates(i)
+
+          val oldSize = set.size
+          for (j <- 0 until transPreStates.size)
+            if (set contains j)
+              set |= transPreStates(j)
+
+          if (set.size > oldSize)
+            changed = true
+        }
+      }
+
+      transPreStates
+    }
+
+    val initialStateInd = state2Index(initialState)
+
+    ////////////////////////////////////////////////////////////////////////////
+
+    disjFor(for (finalState <- acceptingStates)
+            yield (uniqueLengthStates get finalState) match {
+
+    case Some(len) =>
+      v(0) === len
+
+    case None => {
+      val finalStateInd = state2Index(finalState)
+      val refStates = transPreStates(finalStateInd)
+
+      val productions : List[(Int, Option[Int])] =
+        (if (refStates contains initialStateInd)
+           List((initialStateInd, None))
+         else List()) :::
+        (for (state <- refStates.iterator;
+              preState <- preStates(state).iterator)
+         yield (state, Some(preState))).toList
+
+      val (prodVars, zVars, sizeVar) = {
+        val prodVars = for ((_, num) <- productions.zipWithIndex) yield v(num)
+        var nextVar = prodVars.size
+        val zVars = (for (state <- refStates.iterator) yield {
+          val ind = nextVar
+          nextVar = nextVar + 1
+          state -> v(ind)
+        }).toMap
+        (prodVars, zVars, v(nextVar))
+      }
+
+      // equations relating the production counters
+      val prodEqs =
+        (for (state <- refStates.iterator) yield {
+          LinearCombination(
+             (if (state == finalStateInd)
+                Iterator((IdealInt.ONE, OneTerm))
+              else
+                Iterator.empty) ++
+             (for (((source, targets), prodVar) <-
+                      productions.iterator zip prodVars.iterator;
+                    mult = (if (targets contains state) 1 else 0) -
+                           (if (source == state) 1 else 0))
+              yield (IdealInt(mult), prodVar)),
+             order)
+        }).toList
+
+      val sizeEq =
+        LinearCombination(
+          (for (((_, Some(_)), v) <- productions.iterator zip prodVars.iterator)
+           yield (IdealInt.ONE, v)) ++
+          Iterator((IdealInt.MINUS_ONE, sizeVar)),
+          order)
+
+      val entryZEq =
+        zVars(finalStateInd) - 1
+
+      val allEqs = eqZ(entryZEq :: sizeEq :: prodEqs)
+
+      val prodNonNeg =
+        prodVars >= 0
+
+      val prodImps =
+        (for (((source, _), prodVar) <-
+                productions.iterator zip prodVars.iterator;
+              if source != finalStateInd)
+         yield ((prodVar === 0) | (zVars(source) > 0))).toList
+
+      val zImps =
+        (for (state <- refStates.iterator; if state != finalStateInd) yield {
+           disjFor(Iterator(zVars(state) === 0) ++
+                   (for (((source, targets), prodVar) <-
+                           productions.iterator zip prodVars.iterator;
+                         if targets contains state)
+                    yield conj(zVars(state) === zVars(source) + 1,
+                               geqZ(List(prodVar - 1, zVars(source) - 1)))))
+         }).toList
+
+      val matrix =
+        conj(allEqs :: prodNonNeg :: prodImps ::: zImps)
+      val rawConstraint =
+        exists(prodVars.size + zVars.size, matrix)
+
+      val constraint =
+        ap.util.Timeout.withTimeoutMillis(1000) {
+          // best-effort attempt to get a quantifier-free version of the
+          // length abstraction
+          PresburgerTools.elimQuantifiersWithPreds(rawConstraint)
+        } {
+          ReduceWithConjunction(Conjunction.TRUE, order)(rawConstraint)
+        }
+
+      constraint
+    }})
   }
 }
 
diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
index 13ae3866fa..8247bfe6f0 100644
--- a/src/test/scala/SMTLIBTests.scala
+++ b/src/test/scala/SMTLIBTests.scala
@@ -3,7 +3,7 @@ package ostrich
 import ap.CmdlMain
 import ap.DialogUtil.asString
 
-import org.scalacheck.{Arbitrary, Gen, Properties}
+import org.scalacheck.Properties
 import org.scalacheck.Prop._
 
 object SMTLIBTests extends Properties("SMTLIBTests") {

From b2c5e6e5423ed72a0d71911bdd36da0fc526f5a5 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Tue, 23 Mar 2021 14:27:58 +0100
Subject: [PATCH 18/27] Make the SMTLib tests more verbose on failure

---
 src/test/scala/SMTLIBTests.scala | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/test/scala/SMTLIBTests.scala b/src/test/scala/SMTLIBTests.scala
index 8247bfe6f0..b0e1f572c3 100644
--- a/src/test/scala/SMTLIBTests.scala
+++ b/src/test/scala/SMTLIBTests.scala
@@ -18,8 +18,13 @@ object SMTLIBTests extends Properties("SMTLIBTests") {
     expResult match {
       case "error" =>
         (result split "\n") exists { str => str contains "error" }
-      case res =>
-        (result split "\n") contains res
+      case res => {
+        // FIXME There is almost guaranteed to be a better way to debug this,
+        // but it beats me.
+        val doesMatch = (result split "\n") contains res
+        if(!doesMatch) println(result.strip())
+        doesMatch
+      }
     }
   }
 

From 7077ec12b27444bf89fc3e32e25742ad5bfc3592 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Wed, 24 Mar 2021 13:39:12 +0100
Subject: [PATCH 19/27] Add a gitignore file

---
 .gitignore | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 .gitignore

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000..7def4b01ad
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,7 @@
+/target
+.bloop
+/.bsp
+/.metals
+.DS_Store
+/project/project
+/project/target
\ No newline at end of file

From 6168f159176ba970574e5b607a3305d513c813b3 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Wed, 24 Mar 2021 14:03:51 +0100
Subject: [PATCH 20/27] Bug: can't match against Seq for ArrayBuffer in 2.13

---
 src/main/scala/ostrich/Exploration.scala | 17 +++++++----------
 1 file changed, 7 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 6cf2a5e5ab..42eb0f7560 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -762,24 +762,21 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
       AutomataUtils.product(constraints, _flags.minimizeAutomata)
 
     def ensureCompleteLengthConstraints : Unit =
-      constraints match {
-        case Seq() | Seq(_) =>
-          // nothing, all length constraints already pushed
-        case auts =>
-          addLengthConstraint(TermConstraint(t, intersection),
-                              for (a <- constraints.toSeq)
-                              yield TermConstraint(t, a))
-      }
+      if (!constraints.isEmpty) {
+        addLengthConstraint(TermConstraint(t, intersection),
+                            for (a <- constraints.toSeq)
+                            yield TermConstraint(t, a))
+      } // nothing, all length constraints already pushed
 
     def getAcceptedWord : Seq[Int] =
       constraints match {
-        case Seq() => List()
+        case _ if constraints.isEmpty => List()
         case auts  => intersection.getAcceptedWord.get.toSeq
       }
 
     def getAcceptedWordLen(len : Int) : Seq[Int] =
       constraints match {
-        case Seq() => for (_ <- 0 until len) yield 0
+        case _ if constraints.isEmpty => for (_ <- 0 until len) yield 0
         case auts  => AutomataUtils.findAcceptedWord(auts.toSeq, len).get
       }
   }

From 919d59a48157d0f41775e1a8179d2abc796587c6 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Tue, 23 Mar 2021 12:32:50 +0100
Subject: [PATCH 21/27] Add back the Parikh Theory

---
 build.sbt                              |   3 +-
 src/main/scala/ostrich/Automaton.scala | 172 +++----------------------
 2 files changed, 20 insertions(+), 155 deletions(-)

diff --git a/build.sbt b/build.sbt
index c1fa0d95e6..bacaea16b6 100644
--- a/build.sbt
+++ b/build.sbt
@@ -19,7 +19,8 @@ lazy val commonSettings = Seq(
   libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT",
   libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.5",
   libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.0" % "test",
-  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8"
+  libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8",
+  libraryDependencies += "uuverifiers" %% "parikh-theory" % "0.1.0-SNAPSHOT"
 )
 
 lazy val root = (project in file(".")).
diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index 5e6fab762e..0b2fd42a71 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -32,16 +32,17 @@
 
 package ostrich
 
-import ap.basetypes.IdealInt
-import ap.PresburgerTools
-import ap.terfor.{Formula, TerForConvenience, TermOrder, OneTerm}
-import ap.terfor.linearcombination.LinearCombination
-import ap.terfor.conjunctions.{Conjunction, ReduceWithConjunction}
-
-import scala.collection.mutable.{BitSet => MBitSet,
-                                 HashMap => MHashMap, HashSet => MHashSet,
+import ap.terfor.{Formula, TerForConvenience, TermOrder}
+
+import scala.collection.mutable.{HashMap => MHashMap,
+  HashSet => MHashSet,
   ArrayStack}
 
+import uuverifiers.parikh_theory.{
+  Automaton => OtherAutomaton,
+  LengthCounting
+}
+
 /**
  * Interface for different implementations of finite-state automata.
  */
@@ -191,7 +192,7 @@ trait TLabelEnumerator[TLabel] {
  * don't have any structure and are not composite, there is a unique
  * initial state, and a set of accepting states.
  */
-trait AtomicStateAutomaton extends Automaton  {
+trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   /**
    * Type of states
    */
@@ -260,7 +261,7 @@ trait AtomicStateAutomaton extends Automaton  {
   /**
    * Iterate over all transitions
    */
-  def transitions : Iterator[(State, TLabel, State)] =
+  override def transitions : Iterator[(State, TLabel, State)] =
     for (s1 <- states.iterator; (s2, lbl) <- outgoingTransitions(s1))
     yield (s1, lbl, s2)
 
@@ -296,7 +297,7 @@ trait AtomicStateAutomaton extends Automaton  {
     todo push initialState
 
     while (!todo.isEmpty) {
-      val s = todo.pop
+      val s = todo.pop()
       if (nonUniqueLengthStates contains s) {
         for ((to, _) <- outgoingTransitions(s)) {
           uniqueLengthStates -= to
@@ -332,157 +333,20 @@ trait AtomicStateAutomaton extends Automaton  {
   lazy val uniqueAcceptedWordLength : Option[Int] = {
     val lengths = for (s <- acceptingStates) yield (uniqueLengthStates get s)
     if (lengths.size == 1 && !(lengths contains None))
-      lengths.iterator.next
+      lengths.iterator.next()
     else
       None
   }
 
   /**
-   * Compute the length abstraction of this automaton. Special case of
-   * Parikh images, following the procedure in Verma et al, CADE 2005
-   */
-   lazy val getLengthAbstraction : Formula = /* Exploration.measure("length abstraction") */ {
+    * Compute the length abstraction of this automaton.
+    */
+  lazy val getLengthAbstraction: Formula = {
     import TerForConvenience._
     implicit val order = TermOrder.EMPTY
 
-    val stateSeq = states.toIndexedSeq
-    val state2Index = stateSeq.iterator.zipWithIndex.toMap
-
-    lazy val preStates = {
-      val preStates = Array.fill(stateSeq.size)(new MBitSet)
-
-      for ((from, _, to) <- transitions)
-        preStates(state2Index(to)) += state2Index(from)
-
-      preStates
-    }
-
-    lazy val transPreStates = {
-      val transPreStates = Array.fill(stateSeq.size)(new MBitSet)
-
-      for ((s1, s2) <- preStates.iterator zip transPreStates.iterator)
-        s2 ++= s1
-
-      for ((s, n) <- transPreStates.iterator.zipWithIndex)
-        s += n
-
-      // fixed-point iterator, to find transitively referenced states
-      var changed = true
-      while (changed) {
-        changed = false
-
-        for (i <- 0 until transPreStates.size) {
-          val set = transPreStates(i)
-
-          val oldSize = set.size
-          for (j <- 0 until transPreStates.size)
-            if (set contains j)
-              set |= transPreStates(j)
-
-          if (set.size > oldSize)
-            changed = true
-        }
-      }
-
-      transPreStates
-    }
-
-    val initialStateInd = state2Index(initialState)
-
-    ////////////////////////////////////////////////////////////////////////////
-
-    disjFor(for (finalState <- acceptingStates)
-            yield (uniqueLengthStates get finalState) match {
-
-    case Some(len) =>
-      v(0) === len
-
-    case None => {
-      val finalStateInd = state2Index(finalState)
-      val refStates = transPreStates(finalStateInd)
-
-      val productions : List[(Int, Option[Int])] =
-        (if (refStates contains initialStateInd)
-           List((initialStateInd, None))
-         else List()) :::
-        (for (state <- refStates.iterator;
-              preState <- preStates(state).iterator)
-         yield (state, Some(preState))).toList
-
-      val (prodVars, zVars, sizeVar) = {
-        val prodVars = for ((_, num) <- productions.zipWithIndex) yield v(num)
-        var nextVar = prodVars.size
-        val zVars = (for (state <- refStates.iterator) yield {
-          val ind = nextVar
-          nextVar = nextVar + 1
-          state -> v(ind)
-        }).toMap
-        (prodVars, zVars, v(nextVar))
-      }
-
-      // equations relating the production counters
-      val prodEqs =
-        (for (state <- refStates.iterator) yield {
-          LinearCombination(
-             (if (state == finalStateInd)
-                Iterator((IdealInt.ONE, OneTerm))
-              else
-                Iterator.empty) ++
-             (for (((source, targets), prodVar) <-
-                      productions.iterator zip prodVars.iterator;
-                    mult = (if (targets contains state) 1 else 0) -
-                           (if (source == state) 1 else 0))
-              yield (IdealInt(mult), prodVar)),
-             order)
-        }).toList
-
-      val sizeEq =
-        LinearCombination(
-          (for (((_, Some(_)), v) <- productions.iterator zip prodVars.iterator)
-           yield (IdealInt.ONE, v)) ++
-          Iterator((IdealInt.MINUS_ONE, sizeVar)),
-          order)
-
-      val entryZEq =
-        zVars(finalStateInd) - 1
-
-      val allEqs = eqZ(entryZEq :: sizeEq :: prodEqs)
-
-      val prodNonNeg =
-        prodVars >= 0
-
-      val prodImps =
-        (for (((source, _), prodVar) <-
-                productions.iterator zip prodVars.iterator;
-              if source != finalStateInd)
-         yield ((prodVar === 0) | (zVars(source) > 0))).toList
-
-      val zImps =
-        (for (state <- refStates.iterator; if state != finalStateInd) yield {
-           disjFor(Iterator(zVars(state) === 0) ++
-                   (for (((source, targets), prodVar) <-
-                           productions.iterator zip prodVars.iterator;
-                         if targets contains state)
-                    yield conj(zVars(state) === zVars(source) + 1,
-                               geqZ(List(prodVar - 1, zVars(source) - 1)))))
-         }).toList
-
-      val matrix =
-        conj(allEqs :: prodNonNeg :: prodImps ::: zImps)
-      val rawConstraint =
-        exists(prodVars.size + zVars.size, matrix)
-
-      val constraint =
-        ap.util.Timeout.withTimeoutMillis(1000) {
-          // best-effort attempt to get a quantifier-free version of the
-          // length abstraction
-          PresburgerTools.elimQuantifiersWithPreds(rawConstraint)
-        } {
-          ReduceWithConjunction(Conjunction.TRUE, order)(rawConstraint)
-        }
-
-      constraint
-    }})
+    val length = v(0)
+    (LengthCounting(IndexedSeq(this))) allowsMonoidValues Seq(length)
   }
 }
 

From 92e6296a27e6fa454c2d03cd3181e15a03e7df70 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Tue, 23 Mar 2021 18:13:45 +0100
Subject: [PATCH 22/27] Slightly cleaner theory invocation (that still doesn't
 work)

---
 src/main/scala/ostrich/Automaton.scala | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index 0b2fd42a71..cb7854c766 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -342,11 +342,10 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
     * Compute the length abstraction of this automaton.
     */
   lazy val getLengthAbstraction: Formula = {
-    import TerForConvenience._
-    implicit val order = TermOrder.EMPTY
+    val lengthTheory = LengthCounting(IndexedSeq(this))
 
-    val length = v(0)
-    (LengthCounting(IndexedSeq(this))) allowsMonoidValues Seq(length)
+    val length = TerForConvenience.v(0)
+    lengthTheory.allowsMonoidValues(Seq(length))(TermOrder.EMPTY)
   }
 }
 

From 89dc0035b1baff6bee4406740127c4f90f46362a Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Wed, 24 Mar 2021 13:06:53 +0100
Subject: [PATCH 23/27] Change the generation of length constraints to support
 new variant

---
 src/main/scala/ostrich/Automaton.scala   | 18 ++++++++++--------
 src/main/scala/ostrich/Exploration.scala |  6 ++----
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index cb7854c766..89dcd046e7 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -32,7 +32,8 @@
 
 package ostrich
 
-import ap.terfor.{Formula, TerForConvenience, TermOrder}
+import ap.terfor.Term
+import ap.SimpleAPI
 
 import scala.collection.mutable.{HashMap => MHashMap,
   HashSet => MHashSet,
@@ -80,9 +81,9 @@ trait Automaton {
   def getAcceptedWord : Option[Seq[Int]]
 
   /**
-   * Compute the length abstraction of this automaton.
+   * Compute the length abstraction of this automaton and assert it into a prover.
    */
-  def getLengthAbstraction : Formula
+  def assertLengthConstraint(lengthTerm: Term, prover: SimpleAPI) : Unit
 
 }
 
@@ -338,14 +339,15 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
       None
   }
 
+  // Spare us running multiple instantiations (it might be expensive)
+  lazy private val lengthTheory = LengthCounting(IndexedSeq(this))
+
   /**
     * Compute the length abstraction of this automaton.
     */
-  lazy val getLengthAbstraction: Formula = {
-    val lengthTheory = LengthCounting(IndexedSeq(this))
-
-    val length = TerForConvenience.v(0)
-    lengthTheory.allowsMonoidValues(Seq(length))(TermOrder.EMPTY)
+  def assertLengthConstraint(lengthTerm: Term, prover: SimpleAPI): Unit = {
+    prover addTheory lengthTheory // Assumption: addTheory is idempotent.
+    prover addAssertion (lengthTheory.allowsMonoidValues(Seq(lengthTerm))(prover.order))
   }
 }
 
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 42eb0f7560..3c978f10c1 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -275,8 +275,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
 
     for (p <- lengthProver) {
       for ((t, aut) <- allInitialConstraints)
-        p addAssertion VariableSubst(0, List(lengthVars(t)), p.order)(
-                                               aut.getLengthAbstraction)
+        aut.assertLengthConstraint(lengthVars(t), p)
 
       if (measure("check length consistency") { p.??? } == ProverStatus.Unsat)
         return None
@@ -517,8 +516,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
       lengthPartitions += sources
       p setPartitionNumber lengthPartitions.size
       val TermConstraint(t, aut) = constraint
-      p addAssertion VariableSubst(0, List(lengthVars(t)), p.order)(
-                                                  aut.getLengthAbstraction)
+      aut.assertLengthConstraint(lengthVars(t), p)
     }
 
   private def checkLengthConsistency : Option[Seq[TermConstraint]] =

From 9ae315fbfe380956f6f1abd70699867653c2f454 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Thu, 24 Jun 2021 14:54:23 +0200
Subject: [PATCH 24/27] More adaptations for the new parikh theory

---
 build.sbt                                     |  2 +-
 src/main/scala/ostrich/AutomataAdapters.scala |  2 +-
 src/main/scala/ostrich/BricsAutomaton.scala   |  2 +-
 src/main/scala/ostrich/Exploration.scala      | 51 ++++++++++---------
 src/main/scala/ostrich/OstrichSolver.scala    |  2 +-
 5 files changed, 32 insertions(+), 27 deletions(-)

diff --git a/build.sbt b/build.sbt
index bacaea16b6..4d02a225bf 100644
--- a/build.sbt
+++ b/build.sbt
@@ -9,7 +9,7 @@ lazy val commonSettings = Seq(
     //"-Xfatal-warnings",
     "-unchecked",
     "-Xlint",
-    "-Xelide-below", "FINE",
+    "-Xelide-below", "INFO",
     // "-feature",
     // "-optimize",
     "-Ywarn-dead-code",
diff --git a/src/main/scala/ostrich/AutomataAdapters.scala b/src/main/scala/ostrich/AutomataAdapters.scala
index f0515ff2de..2f087a05b2 100644
--- a/src/main/scala/ostrich/AutomataAdapters.scala
+++ b/src/main/scala/ostrich/AutomataAdapters.scala
@@ -67,7 +67,7 @@ abstract class AtomicStateAutomatonAdapter[A <: AtomicStateAutomaton]
   def unary_! : Automaton =
     !intern(this)
 
-  def isEmpty : Boolean =
+  override def isEmpty : Boolean =
     !AutomataUtils.areConsistentAtomicAutomata(List(this))
 
   def apply(word : Seq[Int]) : Boolean =
diff --git a/src/main/scala/ostrich/BricsAutomaton.scala b/src/main/scala/ostrich/BricsAutomaton.scala
index 9799ef42ea..4a00349aba 100644
--- a/src/main/scala/ostrich/BricsAutomaton.scala
+++ b/src/main/scala/ostrich/BricsAutomaton.scala
@@ -374,7 +374,7 @@ class BricsAutomaton(val underlying : BAutomaton) extends AtomicStateAutomaton {
   /**
    * Check whether this automaton describes the empty language.
    */
-  def isEmpty : Boolean =
+  override def isEmpty : Boolean =
     underlying.isEmpty
 
   /**
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 3c978f10c1..43362ca4d5 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -37,8 +37,8 @@ import SimpleAPI.ProverStatus
 import ap.basetypes.IdealInt
 import ap.terfor.{Term, ConstantTerm, OneTerm}
 import ap.terfor.linearcombination.LinearCombination
-import ap.terfor.substitutions.VariableSubst
 import ap.util.Seqs
+import uuverifiers.parikh_theory.LengthCounting
 
 import scala.collection.mutable.{HashMap => MHashMap, ArrayBuffer, ArrayStack,
                                  HashSet => MHashSet, LinkedHashSet,
@@ -121,7 +121,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
                            val initialConstraints : Seq[(Term, Automaton)],
                            strDatabase : StrDatabase,
                            lengthProver : Option[SimpleAPI],
-                           lengthVars : Map[Term, Term],
+                           val lengthVars : Map[Term, Term],
                            strictLengths : Boolean,
                            flags : OFlags) {
 
@@ -263,6 +263,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
    * to an integer, and each string variable to a list of characters.
    */
   def findModel : Option[Map[Term, Either[IdealInt, Seq[Int]]]] = {
+    Console.err.println("findModel")
     for (t <- allTerms)
       constraintStores.put(t, newStore(t))
 
@@ -277,8 +278,11 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
       for ((t, aut) <- allInitialConstraints)
         aut.assertLengthConstraint(lengthVars(t), p)
 
-      if (measure("check length consistency") { p.??? } == ProverStatus.Unsat)
+      if (measure("check length consistency") { p.??? } == ProverStatus.Unsat) {
+        Console.err.println("hello!")
+        Console.err.println(p.certificateAsString(Map(), ap.parameters.Param.InputFormat.SMTLIB))
         return None
+      }
     }
 
     if (flags.forwardApprox)
@@ -510,27 +514,34 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
   private val lengthPartitionStack = new ArrayStack[Int]
   private val lengthPartitions = new ArrayBuffer[Seq[TermConstraint]]
 
-  protected def addLengthConstraint(constraint : TermConstraint,
-                                    sources : Seq[TermConstraint]) : Unit =
-    for (p <- lengthProver) {
-      lengthPartitions += sources
-      p setPartitionNumber lengthPartitions.size
-      val TermConstraint(t, aut) = constraint
-      aut.assertLengthConstraint(lengthVars(t), p)
+  protected def addLengthConstraint(lengthTerm : Term,
+                                    sources : Seq[Automaton]) : Unit = {
+    // FIXME cache the theory using Princess LRUcache and/or move to AutomataUtils
+    // FIXME change the type to require AtomicStateAutomaton here
+    val automata = sources.map(_.asInstanceOf[AtomicStateAutomaton]).toIndexedSeq
+    val lengthTheory = LengthCounting(automata)
+
+    for (prover <- lengthProver) {
+      prover addTheory lengthTheory
+      prover addAssertion (lengthTheory.allowsMonoidValues(Seq(lengthTerm))(prover.order))
     }
+  }
 
-  private def checkLengthConsistency : Option[Seq[TermConstraint]] =
+  private def checkLengthConsistency : Option[Seq[TermConstraint]] = {
+    Console.err.println("checkLengthConsistency")
     for (p <- lengthProver;
          if {
            if (debug)
              Console.err.println("checking length consistency")
            measure("check length consistency") {p.???} == ProverStatus.Unsat
          }) yield {
+      Console.err.println(p.certificateAsString(Map(), ap.parameters.Param.InputFormat.SMTLIB))
       for (n <- p.getUnsatCore.toList.sorted;
            if n > 0;
            c <- lengthPartitions(n - 1))
       yield c
     }
+  }
 
   private def pushLengthConstraints : Unit =
     for (p <- lengthProver) {
@@ -598,17 +609,14 @@ class EagerExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
             } else {
               constraints += aut
               currentConstraint = Some(newAut)
-              addLengthConstraint(TermConstraint(t, newAut),
-                                  for (a <- constraints.toSeq)
-                                  yield TermConstraint(t, a))
+              addLengthConstraint(lengthVars(t), constraints.toIndexedSeq)
               None
             }
           }
           case None => {
             constraints += aut
             currentConstraint = Some(aut)
-            val c = TermConstraint(t, aut)
-            addLengthConstraint(c, List(c))
+            addLengthConstraint(lengthVars(t), IndexedSeq(aut))
             None
           }
         }
@@ -744,8 +752,7 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
           case None => {
             constraints += aut
             constraintSet += aut
-            val c = TermConstraint(t, aut)
-            addLengthConstraint(c, List(c))
+            addLengthConstraint(lengthVars(t), IndexedSeq(aut))
             None
           }
         }
@@ -760,12 +767,10 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
       AutomataUtils.product(constraints, _flags.minimizeAutomata)
 
     def ensureCompleteLengthConstraints : Unit =
-      if (!constraints.isEmpty) {
-        addLengthConstraint(TermConstraint(t, intersection),
-                            for (a <- constraints.toSeq)
-                            yield TermConstraint(t, a))
-      } // nothing, all length constraints already pushed
+      if (!constraints.isEmpty) addLengthConstraint(lengthVars(t), constraints.toIndexedSeq)
 
+    // FIXME: how do we delegate this to the theory? I guess we need to be able
+    // to ask the theory with its currently filtered automaton etc etc
     def getAcceptedWord : Seq[Int] =
       constraints match {
         case _ if constraints.isEmpty => List()
diff --git a/src/main/scala/ostrich/OstrichSolver.scala b/src/main/scala/ostrich/OstrichSolver.scala
index 7bbb8a429b..92a52149a0 100644
--- a/src/main/scala/ostrich/OstrichSolver.scala
+++ b/src/main/scala/ostrich/OstrichSolver.scala
@@ -230,7 +230,7 @@ class OstrichSolver(theory : OstrichStringTheory,
     ////////////////////////////////////////////////////////////////////////////
     // Start the actual OSTRICH solver
 
-    SimpleAPI.withProver { lengthProver =>
+    SimpleAPI.withProver(dumpSMT = true) { lengthProver =>
       val lProver =
         if (useLength) {
           lengthProver setConstructProofs true

From 914826032e5b5122a0f60e73a6c973da2cb6cd96 Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Thu, 1 Jul 2021 13:07:20 +0200
Subject: [PATCH 25/27] Hack in support for labels

---
 project/build.properties                    |  1 +
 src/main/scala/ostrich/Automaton.scala      | 43 ++++++++++++++++++---
 src/main/scala/ostrich/BricsAutomaton.scala |  4 ++
 src/main/scala/ostrich/Exploration.scala    |  2 +-
 4 files changed, 44 insertions(+), 6 deletions(-)
 create mode 100644 project/build.properties

diff --git a/project/build.properties b/project/build.properties
new file mode 100644
index 0000000000..67d27a1dfe
--- /dev/null
+++ b/project/build.properties
@@ -0,0 +1 @@
+sbt.version=1.5.3
diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index 89dcd046e7..18f5b1473e 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -41,7 +41,8 @@ import scala.collection.mutable.{HashMap => MHashMap,
 
 import uuverifiers.parikh_theory.{
   Automaton => OtherAutomaton,
-  LengthCounting
+  LengthCounting,
+  SymbolicLabel
 }
 
 /**
@@ -85,6 +86,8 @@ trait Automaton {
    */
   def assertLengthConstraint(lengthTerm: Term, prover: SimpleAPI) : Unit
 
+  def toAmandaAutomaton(): OtherAutomaton
+
 }
 
 ////////////////////////////////////////////////////////////////////////////////
@@ -154,6 +157,8 @@ trait TLabelOps[TLabel] {
    * Get representation of interval [min,max]
    */
   def interval(min : Char, max : Char) : TLabel
+
+  def labelToSymbolicLabel(label: TLabel): SymbolicLabel
 }
 
 /**
@@ -193,7 +198,7 @@ trait TLabelEnumerator[TLabel] {
  * don't have any structure and are not composite, there is a unique
  * initial state, and a set of accepting states.
  */
-trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
+trait AtomicStateAutomaton extends Automaton {
   /**
    * Type of states
    */
@@ -204,7 +209,7 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
    */
   type TLabel
 
-  type Label = TLabel
+  
 
   /**
    * Operations on labels
@@ -259,10 +264,38 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   //////////////////////////////////////////////////////////////////////////
   // Derived methods
 
+
+
+  /**
+    * I gave up and made these
+    */
+  override lazy val toAmandaAutomaton: OtherAutomaton = {
+    val parent = this
+
+    object AutomatonAdapter extends OtherAutomaton {
+      import uuverifiers.parikh_theory.AutomataTypes.{State => OtherState}
+
+      // This really is not exactly a beautiful solution but let's go.
+      val stateToIndex: Map[parent.State, OtherState] = parent.states.zipWithIndex.toMap
+      lazy val indexToState: Map[OtherState, parent.State] = stateToIndex.map(_.swap)
+
+      val initialState: OtherState = stateToIndex(parent.initialState)
+      def isAccept(s: OtherState): Boolean = parent.isAccept(indexToState(s))
+      def outgoingTransitions(from: OtherState): Iterator[(OtherState, SymbolicLabel)] =
+        parent.outgoingTransitions(indexToState(from)).map{
+          case(s, l) =>
+            (stateToIndex(s), parent.LabelOps.labelToSymbolicLabel(l))
+        }
+      def states: Iterable[OtherState] = parent.states.map(stateToIndex)
+    }
+
+    AutomatonAdapter
+  }
+
   /**
    * Iterate over all transitions
    */
-  override def transitions : Iterator[(State, TLabel, State)] =
+  def transitions : Iterator[(State, TLabel, State)] =
     for (s1 <- states.iterator; (s2, lbl) <- outgoingTransitions(s1))
     yield (s1, lbl, s2)
 
@@ -340,7 +373,7 @@ trait AtomicStateAutomaton extends Automaton with OtherAutomaton {
   }
 
   // Spare us running multiple instantiations (it might be expensive)
-  lazy private val lengthTheory = LengthCounting(IndexedSeq(this))
+  lazy private val lengthTheory = LengthCounting(IndexedSeq(toAmandaAutomaton))
 
   /**
     * Compute the length abstraction of this automaton.
diff --git a/src/main/scala/ostrich/BricsAutomaton.scala b/src/main/scala/ostrich/BricsAutomaton.scala
index 4a00349aba..407df31fd3 100644
--- a/src/main/scala/ostrich/BricsAutomaton.scala
+++ b/src/main/scala/ostrich/BricsAutomaton.scala
@@ -43,6 +43,7 @@ import scala.collection.mutable.{HashMap => MHashMap,
                                  MultiMap => MMultiMap,
                                  Set => MSet}
 import scala.jdk.CollectionConverters._
+import uuverifiers.parikh_theory.SymbolicLabel
 
 object BricsAutomaton {
   private def toBAutomaton(aut : Automaton) : BAutomaton = aut match {
@@ -212,6 +213,9 @@ object BricsTLabelOps extends TLabelOps[(Char, Char)] {
    * Get representation of interval [min,max]
    */
   def interval(min : Char, max : Char) : (Char, Char) = (min, max)
+
+  def labelToSymbolicLabel(label: (Char, Char)): SymbolicLabel =
+    SymbolicLabel(label._1, label._2)
 }
 
 class BricsTLabelEnumerator(labels: Iterator[(Char, Char)])
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 43362ca4d5..59b256adb2 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -518,7 +518,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
                                     sources : Seq[Automaton]) : Unit = {
     // FIXME cache the theory using Princess LRUcache and/or move to AutomataUtils
     // FIXME change the type to require AtomicStateAutomaton here
-    val automata = sources.map(_.asInstanceOf[AtomicStateAutomaton]).toIndexedSeq
+    val automata = sources.map(_.toAmandaAutomaton()).toIndexedSeq
     val lengthTheory = LengthCounting(automata)
 
     for (prover <- lengthProver) {

From 8c0cfa2f4c6c2a82f83b8c4f01e60a577a6889fd Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Thu, 1 Jul 2021 13:21:42 +0200
Subject: [PATCH 26/27] Fix the latest upstream delta for Scala 2.13

```
[warn] 48 deprecations (since 2.13.0)
[warn] 2 deprecations (since 2.13.2)
[warn] 33 deprecations (since 2.13.3)
[warn] 83 deprecations in total; re-run with -deprecation for details
[warn] four warnings found
```

Excellent.
---
 src/main/scala/ostrich/AutomataUtils.scala             | 10 +++++-----
 src/main/scala/ostrich/BricsTransducer.scala           |  2 +-
 .../ostrich/OstrichStringFunctionTranslator.scala      |  6 +++---
 src/main/scala/ostrich/TransducerTranslator.scala      |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/main/scala/ostrich/AutomataUtils.scala b/src/main/scala/ostrich/AutomataUtils.scala
index 57edb57006..6d1290698c 100644
--- a/src/main/scala/ostrich/AutomataUtils.scala
+++ b/src/main/scala/ostrich/AutomataUtils.scala
@@ -226,7 +226,7 @@ object AutomataUtils {
    * Product of a number of given automata
    * The minimize argument enable minimization of the product automaton.
    */
-  def product(auts : Seq[Automaton],
+  def product(auts : Iterable[Automaton],
               minimize : Boolean = false) : Automaton =
     if (auts forall { _.isInstanceOf[AtomicStateAutomaton] }) {
       productWithMap(auts map (_.asInstanceOf[AtomicStateAutomaton]),
@@ -244,7 +244,7 @@ object AutomataUtils {
    * The minimize argument enable minimization of the product automaton,
    * which should only be used if the returned maps are not used.
    */
-  def productWithMap(auts : Seq[AtomicStateAutomaton], minimize : Boolean = false) :
+  def productWithMap(auts : Iterable[AtomicStateAutomaton], minimize : Boolean = false) :
     (AtomicStateAutomaton, Map[Any, Seq[Any]]) = {
     val idMap = Map[Any, Seq[Any]]().withDefault(s => Seq(s))
     productWithMaps(auts.map((_, idMap)), minimize)
@@ -259,7 +259,7 @@ object AutomataUtils {
    * The minimize argument enable minimization of the product automaton,
    * which should only be used if the returned maps are not used.
    */
-  private def productWithMaps(auts : Seq[(AtomicStateAutomaton,
+  private def productWithMaps(auts : Iterable[(AtomicStateAutomaton,
                                          Map[Any, Seq[Any]])],
                               minimize : Boolean = false) :
     (AtomicStateAutomaton, Map[Any, Seq[Any]]) = {
@@ -288,7 +288,7 @@ object AutomataUtils {
    * The minimize argument enable minimization of the product automaton,
    * which should only be used if the returned maps are not used.
    */
-  private def fullProductWithMaps(auts : Seq[(AtomicStateAutomaton,
+  private def fullProductWithMaps(auts : Iterable[(AtomicStateAutomaton,
                                              Map[Any, Seq[Any]])],
                                   minimize : Boolean = false) :
     (AtomicStateAutomaton, Map[Any, Seq[Any]]) = {
@@ -387,7 +387,7 @@ object AutomataUtils {
    * Form product of this automaton with given auts, returns a new
    * automaton
    */
-  def product(auts : Seq[AtomicStateAutomaton]) : AtomicStateAutomaton =
+  def product(auts : Iterable[AtomicStateAutomaton]) : AtomicStateAutomaton =
     productWithMap(auts, true)._1
 
   /**
diff --git a/src/main/scala/ostrich/BricsTransducer.scala b/src/main/scala/ostrich/BricsTransducer.scala
index 502bb91e36..5b3b12a748 100644
--- a/src/main/scala/ostrich/BricsTransducer.scala
+++ b/src/main/scala/ostrich/BricsTransducer.scala
@@ -679,7 +679,7 @@ class BricsTransducer(val initialState : BricsAutomaton#State,
     return None
   }
 
-  override def toDot() : String = {
+  override def toDot: String = {
     val sb = new StringBuilder()
     sb.append("digraph transducer {\n")
 
diff --git a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
index 0de5f94b98..09a10ab81e 100644
--- a/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
+++ b/src/main/scala/ostrich/OstrichStringFunctionTranslator.scala
@@ -100,7 +100,7 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
           override def lengthApproximation(arguments : Seq[Term], result : Term,
                                            order : TermOrder) : Formula = {
             import TerForConvenience._
-            implicit val _ = order
+            implicit val o = order
             result >= 0 & result <= 1 &
             ((arguments(0)) <= ind <=> (result === 0))
           }
@@ -118,7 +118,7 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
           override def lengthApproximation(arguments : Seq[Term], result : Term,
                                            order : TermOrder) : Formula = {
             import TerForConvenience._
-            implicit val _ = order
+            implicit val o = order
             result >= 0 & result <= 1 &
             ((arguments(0)) <= ind <=> (result === 0))
           }
@@ -138,7 +138,7 @@ class OstrichStringFunctionTranslator(theory : OstrichStringTheory,
           override def lengthApproximation(arguments : Seq[Term], result : Term,
                                            order : TermOrder) : Formula = {
             import TerForConvenience._
-            implicit val _ = order
+            implicit val o = order
             ((arguments(0) >= trimLeft + trimRight) &
                result === arguments(0) - (trimLeft + trimRight)) |
             ((arguments(0) < trimLeft + trimRight) &
diff --git a/src/main/scala/ostrich/TransducerTranslator.scala b/src/main/scala/ostrich/TransducerTranslator.scala
index 4ec9070f47..8420a94f64 100644
--- a/src/main/scala/ostrich/TransducerTranslator.scala
+++ b/src/main/scala/ostrich/TransducerTranslator.scala
@@ -210,7 +210,7 @@ object TransducerTranslator {
         new Iterator[IdealInt] {
           def hasNext : Boolean =
             (??? == ProverStatus.Sat)
-          def next : IdealInt = {
+          def next(): IdealInt = {
             ???
             val res = eval(outputC)
             !! (outputC =/= res)

From 37872290816d643520620a9d099b0ef4383cf16a Mon Sep 17 00:00:00 2001
From: Amanda Stjerna <amanda.stjerna@it.uu.se>
Date: Thu, 15 Jul 2021 15:18:57 +0200
Subject: [PATCH 27/27] Fix compatibility issues, finish integrating into
 parikh theory

---
 .sbtconfig                                    |  3 ++
 .scalafmt.conf                                |  6 ++++
 .vscode/launch.json                           | 23 ++++++++++++++
 .vscode/settings.json                         |  5 +++
 build.sbt                                     | 30 +++++++++++-------
 project/metals.sbt                            |  4 +++
 src/main/scala/ostrich/AutomataUtils.scala    |  4 +--
 src/main/scala/ostrich/Automaton.scala        |  9 +++---
 src/main/scala/ostrich/BricsTransducer.scala  |  4 +--
 src/main/scala/ostrich/Exploration.scala      | 31 ++++++++-----------
 src/main/scala/ostrich/OstrichSolver.scala    |  2 +-
 .../scala/ostrich/OstrichStringTheory.scala   | 28 +++++------------
 12 files changed, 87 insertions(+), 62 deletions(-)
 create mode 100644 .sbtconfig
 create mode 100644 .scalafmt.conf
 create mode 100644 .vscode/launch.json
 create mode 100644 .vscode/settings.json
 create mode 100644 project/metals.sbt

diff --git a/.sbtconfig b/.sbtconfig
new file mode 100644
index 0000000000..0d15dac5bd
--- /dev/null
+++ b/.sbtconfig
@@ -0,0 +1,3 @@
+SBT_OPTS="-Xms4G -Xmx4G -Xss2M 
+ -XX:+CMSClassUnloadingEnabled 
+ -XX:MaxPermSize=4G"
\ No newline at end of file
diff --git a/.scalafmt.conf b/.scalafmt.conf
new file mode 100644
index 0000000000..bd7749b5ad
--- /dev/null
+++ b/.scalafmt.conf
@@ -0,0 +1,6 @@
+maxColumn = 80
+version=2.2.1
+project.git = true
+docstrings = "JavaDoc"
+# rewrite.rules = [SortImports]
+spaces.beforeContextBoundColon=Always
\ No newline at end of file
diff --git a/.vscode/launch.json b/.vscode/launch.json
new file mode 100644
index 0000000000..7e5d21aa5e
--- /dev/null
+++ b/.vscode/launch.json
@@ -0,0 +1,23 @@
+{
+    // Use IntelliSense to learn about possible attributes.
+    // Hover to view descriptions of existing attributes.
+    // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387
+    "version": "0.2.0",
+    "configurations": [
+        {
+            "type": "scala",
+            "request": "launch",
+            "name": "Run tests",
+            "testClass": "ostrich.APITest",
+            "buildTarget": "root"
+        },
+        {
+            "type": "scala",
+            "name": "Debug ostrich.OstrichMain",
+            "request": "launch",
+            "mainClass": "ostrich.OstrichMain",
+            "buildTarget": "root",
+            "args": ["+quiet", "-stringSolver=ostrich.OstrichStringTheory:+eager", "tests/concat-regex.smt2"]
+        }
+    ]
+}
\ No newline at end of file
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 0000000000..32cfc61d28
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,5 @@
+{
+    "files.watcherExclude": {
+        "**/target": true
+    }
+}
\ No newline at end of file
diff --git a/build.sbt b/build.sbt
index 4d02a225bf..ed4fa35c16 100644
--- a/build.sbt
+++ b/build.sbt
@@ -3,29 +3,35 @@ lazy val commonSettings = Seq(
   organization := "uuverifiers",
   version := "1.0",
   scalaVersion := "2.13.5",
-  publishTo := Some(Resolver.file("file",  new File( "/home/wv/public_html/maven/" )) ),
+  publishTo := Some(
+    Resolver.file("file", new File("/home/wv/public_html/maven/"))
+  ),
   scalacOptions ++= Seq(
     "-deprecation",
     //"-Xfatal-warnings",
     "-unchecked",
     "-Xlint",
-    "-Xelide-below", "INFO",
-    // "-feature",
-    // "-optimize",
+    "-Xelide-below",
+    "INFO",
+    "-feature",
+    "-opt-inline-from:**",
+    "-opt:l:method",
+    "-opt:l:inline",
     "-Ywarn-dead-code",
     "-Ywarn-unused"
   ),
-  resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/").withAllowInsecureProtocol(true),
-  libraryDependencies += "uuverifiers" %% "princess" % "nightly-SNAPSHOT",
+  resolvers += ("uuverifiers" at "http://logicrunch.research.it.uu.se/maven/")
+    .withAllowInsecureProtocol(true),
+  libraryDependencies += "uuverifiers" %% "princess" % "nightlySNAPSHOT",
   libraryDependencies += "uuverifiers" % "ecma2020-regex-parser" % "0.5",
   libraryDependencies += "org.scalacheck" %% "scalacheck" % "1.14.0" % "test",
   libraryDependencies += "dk.brics.automaton" % "automaton" % "1.11-8",
   libraryDependencies += "uuverifiers" %% "parikh-theory" % "0.1.0-SNAPSHOT"
 )
 
-lazy val root = (project in file(".")).
-  settings(commonSettings: _*).
-  settings(
-    mainClass in Compile := Some("ostrich.OstrichMain"),
-    unmanagedSourceDirectories in Test += baseDirectory.value / "replaceall-benchmarks" / "src" / "test" / "scala"
-  )
+lazy val root = (project in file("."))
+  .settings(commonSettings: _*)
+  .settings(
+    Compile / mainClass := Some("ostrich.OstrichMain"),
+    Test / unmanagedSourceDirectories += baseDirectory.value / "replaceall-benchmarks" / "src" / "test" / "scala"
+  )
\ No newline at end of file
diff --git a/project/metals.sbt b/project/metals.sbt
new file mode 100644
index 0000000000..1d4c14ce8e
--- /dev/null
+++ b/project/metals.sbt
@@ -0,0 +1,4 @@
+// DO NOT EDIT! This file is auto-generated.
+// This file enables sbt-bloop to create bloop config files.
+
+addSbtPlugin("ch.epfl.scala" % "sbt-bloop" % "1.4.8-19-4d9f966b")
diff --git a/src/main/scala/ostrich/AutomataUtils.scala b/src/main/scala/ostrich/AutomataUtils.scala
index 6d1290698c..93cad5291f 100644
--- a/src/main/scala/ostrich/AutomataUtils.scala
+++ b/src/main/scala/ostrich/AutomataUtils.scala
@@ -154,7 +154,7 @@ object AutomataUtils {
    * The automata are required to all have the same label type (though this is
    * not checked statically)
    */
-  def findAcceptedWordAtomic(auts : Seq[AtomicStateAutomaton],
+  def findAcceptedWordAtomic(auts : Iterable[AtomicStateAutomaton],
                              len : Int) : Option[Seq[Int]] = {
     val autsList = auts.toList
     val headAut = autsList.head
@@ -216,7 +216,7 @@ object AutomataUtils {
    * Check whether there is some word of length <code>len</code> accepted
    * by all of the given automata.
    */
-  def findAcceptedWord(auts : Seq[Automaton],
+  def findAcceptedWord(auts : Iterable[Automaton],
                        len : Int) : Option[Seq[Int]] =
     findAcceptedWordAtomic(for (aut <- auts)
                              yield aut.asInstanceOf[AtomicStateAutomaton],
diff --git a/src/main/scala/ostrich/Automaton.scala b/src/main/scala/ostrich/Automaton.scala
index 18f5b1473e..582326647d 100644
--- a/src/main/scala/ostrich/Automaton.scala
+++ b/src/main/scala/ostrich/Automaton.scala
@@ -42,7 +42,8 @@ import scala.collection.mutable.{HashMap => MHashMap,
 import uuverifiers.parikh_theory.{
   Automaton => OtherAutomaton,
   LengthCounting,
-  SymbolicLabel
+  SymbolicLabel, 
+  Tracing
 }
 
 /**
@@ -198,7 +199,7 @@ trait TLabelEnumerator[TLabel] {
  * don't have any structure and are not composite, there is a unique
  * initial state, and a set of accepting states.
  */
-trait AtomicStateAutomaton extends Automaton {
+trait AtomicStateAutomaton extends Automaton with Tracing {
   /**
    * Type of states
    */
@@ -269,9 +270,8 @@ trait AtomicStateAutomaton extends Automaton {
   /**
     * I gave up and made these
     */
-  override lazy val toAmandaAutomaton: OtherAutomaton = {
+  override lazy val toAmandaAutomaton: OtherAutomaton = trace("toAmandaAutomaton"){
     val parent = this
-
     object AutomatonAdapter extends OtherAutomaton {
       import uuverifiers.parikh_theory.AutomataTypes.{State => OtherState}
 
@@ -288,7 +288,6 @@ trait AtomicStateAutomaton extends Automaton {
         }
       def states: Iterable[OtherState] = parent.states.map(stateToIndex)
     }
-
     AutomatonAdapter
   }
 
diff --git a/src/main/scala/ostrich/BricsTransducer.scala b/src/main/scala/ostrich/BricsTransducer.scala
index 5b3b12a748..eafddd8ab9 100644
--- a/src/main/scala/ostrich/BricsTransducer.scala
+++ b/src/main/scala/ostrich/BricsTransducer.scala
@@ -39,9 +39,7 @@ import scala.collection.mutable.{HashSet => MHashSet,
                                  MultiMap => MMultiMap,
                                  Set => MSet}
 
-import dk.brics.automaton.{Automaton => BAutomaton,
-                           State => BState,
-                           Transition => BTransition}
+import dk.brics.automaton.{State => BState}
 
 
 import java.lang.StringBuilder
diff --git a/src/main/scala/ostrich/Exploration.scala b/src/main/scala/ostrich/Exploration.scala
index 59b256adb2..425b4f6efe 100644
--- a/src/main/scala/ostrich/Exploration.scala
+++ b/src/main/scala/ostrich/Exploration.scala
@@ -279,8 +279,6 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
         aut.assertLengthConstraint(lengthVars(t), p)
 
       if (measure("check length consistency") { p.??? } == ProverStatus.Unsat) {
-        Console.err.println("hello!")
-        Console.err.println(p.certificateAsString(Map(), ap.parameters.Param.InputFormat.SMTLIB))
         return None
       }
     }
@@ -332,7 +330,6 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
 
   private def dfExplore(apps : List[(PreOp, Seq[Term], Term)])
                       : ConflictSet = apps match {
-
     case List() => {
       if (debug)
         Console.err.println("Trying to contruct model")
@@ -442,7 +439,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
       while (measure("pre-op hasNext") {newConstraintsIt.hasNext}) {
         ap.util.Timeout.check
 
-        val argCS = measure("pre-op next") {newConstraintsIt.next}
+        val argCS = measure("pre-op next") {newConstraintsIt.next()}
 
         for (a <- args)
           constraintStores(a).push
@@ -515,7 +512,7 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
   private val lengthPartitions = new ArrayBuffer[Seq[TermConstraint]]
 
   protected def addLengthConstraint(lengthTerm : Term,
-                                    sources : Seq[Automaton]) : Unit = {
+                                    sources : Seq[Automaton]): Unit = {
     // FIXME cache the theory using Princess LRUcache and/or move to AutomataUtils
     // FIXME change the type to require AtomicStateAutomaton here
     val automata = sources.map(_.toAmandaAutomaton()).toIndexedSeq
@@ -528,14 +525,11 @@ abstract class Exploration(val funApps : Seq[(PreOp, Seq[Term], Term)],
   }
 
   private def checkLengthConsistency : Option[Seq[TermConstraint]] = {
-    Console.err.println("checkLengthConsistency")
     for (p <- lengthProver;
          if {
-           if (debug)
-             Console.err.println("checking length consistency")
-           measure("check length consistency") {p.???} == ProverStatus.Unsat
+           measure("check length consistency") {p.???}
+           p.??? == ProverStatus.Unsat
          }) yield {
-      Console.err.println(p.certificateAsString(Map(), ap.parameters.Param.InputFormat.SMTLIB))
       for (n <- p.getUnsatCore.toList.sorted;
            if n > 0;
            c <- lengthPartitions(n - 1))
@@ -609,14 +603,14 @@ class EagerExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
             } else {
               constraints += aut
               currentConstraint = Some(newAut)
-              addLengthConstraint(lengthVars(t), constraints.toIndexedSeq)
+              addLengthConstraint(t, constraints.toIndexedSeq)
               None
             }
           }
           case None => {
             constraints += aut
             currentConstraint = Some(aut)
-            addLengthConstraint(lengthVars(t), IndexedSeq(aut))
+            addLengthConstraint(t, IndexedSeq(aut))
             None
           }
         }
@@ -752,7 +746,7 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
           case None => {
             constraints += aut
             constraintSet += aut
-            addLengthConstraint(lengthVars(t), IndexedSeq(aut))
+            lengthVars.get(t).foreach(addLengthConstraint(_, IndexedSeq(aut)))
             None
           }
         }
@@ -774,14 +768,15 @@ class LazyExploration(_funApps : Seq[(PreOp, Seq[Term], Term)],
     def getAcceptedWord : Seq[Int] =
       constraints match {
         case _ if constraints.isEmpty => List()
-        case auts  => intersection.getAcceptedWord.get.toSeq
+        case _  => intersection.getAcceptedWord.get
       }
 
     def getAcceptedWordLen(len : Int) : Seq[Int] =
-      constraints match {
-        case _ if constraints.isEmpty => for (_ <- 0 until len) yield 0
-        case auts  => AutomataUtils.findAcceptedWord(auts.toSeq, len).get
-      }
+    if(constraints.isEmpty) {
+      for (_ <- 0 until len) yield 0}
+    else {
+      AutomataUtils.findAcceptedWord(constraints, len).get
+    }
   }
 
 }
diff --git a/src/main/scala/ostrich/OstrichSolver.scala b/src/main/scala/ostrich/OstrichSolver.scala
index 92a52149a0..82758bdb3d 100644
--- a/src/main/scala/ostrich/OstrichSolver.scala
+++ b/src/main/scala/ostrich/OstrichSolver.scala
@@ -230,7 +230,7 @@ class OstrichSolver(theory : OstrichStringTheory,
     ////////////////////////////////////////////////////////////////////////////
     // Start the actual OSTRICH solver
 
-    SimpleAPI.withProver(dumpSMT = true) { lengthProver =>
+    SimpleAPI.withProver() { lengthProver =>
       val lProver =
         if (useLength) {
           lengthProver setConstructProofs true
diff --git a/src/main/scala/ostrich/OstrichStringTheory.scala b/src/main/scala/ostrich/OstrichStringTheory.scala
index bd3bec9a61..bf8454b33f 100644
--- a/src/main/scala/ostrich/OstrichStringTheory.scala
+++ b/src/main/scala/ostrich/OstrichStringTheory.scala
@@ -242,28 +242,14 @@ class OstrichStringTheory(transducers : Seq[(String, Transducer)],
       new ap.util.LRUCache[Conjunction,
                            Option[Map[Term, Either[IdealInt, Seq[Int]]]]](3)
 
-    override def handleGoal(goal : Goal)
-                       : Seq[Plugin.Action] = goalState(goal) match {
-
-      case Plugin.GoalState.Final => { //  Console.withOut(Console.err) 
-
-        breakCyclicEquations(goal) match {
-          case Some(actions) =>
-            actions
-          case None =>
-            modelCache(goal.facts) {
-              ostrichSolver.findStringModel(goal)
-            } match {
-              case Some(m) =>
-                equalityPropagator.handleSolution(goal, m)
-              case None =>
-                List(Plugin.AddFormula(Conjunction.TRUE))
-            }
+    override def handleGoal(goal: Goal): Seq[Plugin.Action] =
+      if (goalState(goal) == Plugin.GoalState.Final) {
+        breakCyclicEquations(goal).getOrElse {
+          modelCache(goal.facts)(ostrichSolver.findStringModel(goal))
+            .map(equalityPropagator.handleSolution(goal, _))
+            .getOrElse(List(Plugin.AddFormula(Conjunction.TRUE)))
         }
-      }
-
-      case _ => List()
-    }
+      } else List()
 
     override def generateModel(goal : Goal) : Option[Conjunction] =
       if (Seqs.disjointSeq(goal.facts.predicates, predicates)) {