Update

.gitignore

@@ -2,3 +2,10 @@ target
 
 .*.swp
 *~
+
+.metals
+.bloop
+.vscode
+project/.bloop
+project/metals.sbt
+project/project

.larabot.conf

@@ -1,12 +1,5 @@
 commands = [
-    "sbt -batch ++2.10.7 test"
-    "sbt -batch ++2.11.12 test"
-    "sbt -batch ++2.12.8 test"
-    "sbt -batch ++2.13.0 test"
-    "sbt -batch ++2.10.7 it:test"
-    "sbt -batch ++2.11.12 it:test"
-    "sbt -batch ++2.12.8 it:test"
-    "sbt -batch ++2.13.0 it:test"
+    "sbt -batch ++2.12.13 it:test"
 ]
 
 trusted = [

build.sbt

@@ -8,7 +8,9 @@ javaOptions in IntegrationTest ++= Seq("-Xss128M")
 
 fork in IntegrationTest := true
 
-libraryDependencies += "org.scalatest" %% "scalatest" % "3.0.8" % "test,it"
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7"
+libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.7" % "test"
+
 
 logBuffered in IntegrationTest := false
 
@@ -17,19 +19,13 @@ parallelExecution in Test := true
 lazy val commonSettings = Seq(
   organization := "com.regblanc",
   name := "scala-smtlib",
-  scalaVersion := "2.12.8",
-  crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.13.0")
-)
-
-lazy val publishSettings = Seq(
-  bintrayOrganization := Some("epfl-lara"),
-  bintrayRepository := "maven",
+  scalaVersion := "2.12.13",
+  crossScalaVersions := Seq("2.10.7", "2.11.12", "2.12.8", "2.12.13", "2.13.0", "2.13.5")
 )
 
 lazy val root = (project in file(".")).
   configs(IntegrationTest).
   settings(commonSettings: _*).
-  settings(publishSettings: _*).
   settings(Defaults.itSettings: _*)
 
 publishMavenStyle := true

project/build.properties

@@ -1 +1 @@
-sbt.version=1.2.8
+sbt.version=1.3.0

project/plugins.sbt

@@ -1,6 +1 @@
 addSbtPlugin("com.typesafe.sbt" % "sbt-git" % "1.0.0")
-
-// avoids warning from sbt-git, see https://github.com/sbt/sbt-git#known-issues
-libraryDependencies += "org.slf4j" % "slf4j-nop" % "1.7.21"
-
-addSbtPlugin("org.foundweekends" % "sbt-bintray" % "0.5.4")

src/it/resources/regression/smtlib/solving/cvc4/define_fun2.smt2

@@ -1,5 +1,5 @@
 (set-option :print-success true)
-(set-logic QF_UF)
+(set-logic UF)
 (declare-sort U 0)
 (declare-fun x0 () U)
 (declare-fun y0 () U)

src/it/resources/regression/smtlib/solving/cvc4/define_fun3.smt2

@@ -1,5 +1,5 @@
 (set-option :print-success true)
-(set-logic QF_UF)
+(set-logic UF)
 (declare-sort U 0)
 (declare-fun x0 () U)
 (declare-fun y0 () U)

src/it/scala/smtlib/it/ProcessInterpreterTests.scala

@@ -3,7 +3,7 @@ package it
 
 import scala.sys.process._
 
-import org.scalatest.FunSuite
+import org.scalatest.funsuite.AnyFunSuite
 
 import java.io.File
 import java.io.FileReader
@@ -14,7 +14,7 @@ import printer.RecursivePrinter
 import interpreters._
 
 
-class ProcessInterpreterTests extends FunSuite with TestHelpers {
+class ProcessInterpreterTests extends AnyFunSuite with TestHelpers {
 
   //TODO: properly get all interpreters
   def interpreters: Seq[Interpreter] = Seq(getZ3Interpreter)

src/it/scala/smtlib/it/SmtLibRunnerTests.scala

@@ -3,7 +3,7 @@ package it
 
 import scala.sys.process._
 
-import org.scalatest.FunSuite
+import org.scalatest.funsuite.AnyFunSuite
 
 import java.io.File
 import java.io.FileReader
@@ -21,7 +21,7 @@ import interpreters._
   *
   * TODO: proper way to display warning when not all tests are run because of not found executables.
   */
-class SmtLibRunnerTests extends FunSuite with TestHelpers {
+class SmtLibRunnerTests extends AnyFunSuite with TestHelpers {
 
   filesInResourceDir("regression/smtlib/solving/all", _.endsWith(".smt2")).foreach(file => {
     if(isZ3Available) {
@@ -72,7 +72,7 @@ class SmtLibRunnerTests extends FunSuite with TestHelpers {
     val lexer = new Lexer(new FileReader(file))
     val parser = new Parser(lexer)
 
-    for(expected <- scala.io.Source.fromFile(want).getLines) {
+    for(expected <- scala.io.Source.fromFile(want).getLines()) {
       val cmd = parser.parseCommand
       assert(cmd !== null)
       val res: String = interpreter.eval(cmd).toString

src/it/scala/smtlib/it/TestHelpers.scala

@@ -3,7 +3,7 @@ package it
 
 import scala.sys.process._
 
-import org.scalatest.FunSuite
+import org.scalatest.funsuite.AnyFunSuite
 
 import java.io.File
 import java.io.FileReader

src/it/scala/smtlib/it/TheoriesBuilderTests.scala

@@ -3,7 +3,7 @@ package it
 
 import scala.sys.process._
 
-import org.scalatest.FunSuite
+import org.scalatest.funsuite.AnyFunSuite
 
 import java.io.File
 import java.io.FileReader
@@ -16,7 +16,7 @@ import trees.CommandsResponses._
 
 
 /** Checks that formula build with theories module are correctly handled by solvers */
-class TheoriesBuilderTests extends FunSuite with TestHelpers {
+class TheoriesBuilderTests extends AnyFunSuite with TestHelpers {
 
 
   def mkTest(formula: Term, expectedStatus: Status, prefix: String) = {

src/main/scala/smtlib/extensions/tip/Parser.scala

@@ -38,13 +38,13 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
   override protected def parseTermWithoutParens(startPos: Position): Term = getPeekToken.kind match {
     case Tokens.Lambda =>
       eat(Tokens.Lambda)
-      val args = parseMany(parseSortedVar _)
+      val args = parseMany(() => parseSortedVar)
       val body = parseTerm
       Lambda(args, body)
 
     case Tokens.At =>
       eat(Tokens.At)
-      val (caller +: args) = parseUntil(LT.CParen, eatEnd = false)(parseTerm _)
+      val (caller +: args) = parseUntil(LT.CParen, eatEnd = false)(() => parseTerm)
       Application(caller, args)
 
     case Tokens.Match =>
@@ -59,7 +59,7 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
             Default
 
           case LT.OParen =>
-            val (sym, binders) = parseOneOrMore(parseSymbol _)
+            val (sym, binders) = parseOneOrMore(() => parseSymbol)
             CaseClass(sym, binders)
 
           case _ =>
@@ -82,7 +82,7 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
       getPeekToken.kind match {
         case LT.Par =>
           eat(LT.Par)
-          val tps = parseMany(parseSymbol _)
+          val tps = parseMany(() => parseSymbol)
           val res = parseTerm
           eat(LT.CParen)
           (Some(tps), res)
@@ -123,8 +123,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
         case LT.OParen =>
           eat(LT.OParen)
           eat(LT.Par)
-          val tps = parseMany(parseSymbol _)
-          val (sym, sort) = parseWithin(LT.OParen, LT.CParen)(parseDecl _)
+          val tps = parseMany(() => parseSymbol)
+          val (sym, sort) = parseWithin(LT.OParen, LT.CParen)(() => parseDecl)
           eat(LT.CParen)
           DeclareConstPar(tps, sym, sort)
         case _ =>
@@ -136,16 +136,16 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
       eat(LT.DeclareFun)
       def parseDecl: (SSymbol, Seq[Sort], Sort) = {
         val sym = parseSymbol
-        val sorts = parseMany(parseSort _)
+        val sorts = parseMany(() => parseSort)
         val resultSort = parseSort
         (sym, sorts, resultSort)
       }
       getPeekToken.kind match {
         case LT.OParen =>
           eat(LT.OParen)
           eat(LT.Par)
-          val tps = parseMany(parseSymbol _)
-          val (sym, args, resultSort) = parseWithin(LT.OParen, LT.CParen)(parseDecl _)
+          val tps = parseMany(() => parseSymbol)
+          val (sym, args, resultSort) = parseWithin(LT.OParen, LT.CParen)(() => parseDecl)
           eat(LT.CParen)
           DeclareFunPar(tps, sym, args, resultSort)
         case _ =>
@@ -159,8 +159,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
         case LT.OParen =>
           eat(LT.OParen)
           eat(LT.Par)
-          val tps = parseMany(parseSymbol _)
-          val funDef = parseWithin(LT.OParen, LT.CParen)(parseFunDef _)
+          val tps = parseMany(() => parseSymbol)
+          val funDef = parseWithin(LT.OParen, LT.CParen)(() => parseFunDef)
           eat(LT.CParen)
           DefineFunPar(tps, funDef)
 
@@ -175,8 +175,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
         case LT.OParen =>
           eat(LT.OParen)
           eat(LT.Par)
-          val tps = parseMany(parseSymbol _)
-          val funDef = parseWithin(LT.OParen, LT.CParen)(parseFunDef _)
+          val tps = parseMany(() => parseSymbol)
+          val funDef = parseWithin(LT.OParen, LT.CParen)(() => parseFunDef)
           eat(LT.CParen)
           DefineFunRecPar(tps, funDef)
 
@@ -192,16 +192,16 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
         val funDec = getPeekToken.kind match {
           case LT.Par =>
             eat(LT.Par)
-            val tps = parseMany(parseSymbol _)
-            val funDec = parseWithin(LT.OParen, LT.CParen)(parseFunDec _)
+            val tps = parseMany(() => parseSymbol)
+            val funDec = parseWithin(LT.OParen, LT.CParen)(() => parseFunDec)
             Left(FunDecPar(tps, funDec.name, funDec.params, funDec.returnSort))
           case _ =>
             Right(parseFunDec)
         }
         eat(LT.CParen)
         funDec
       })
-      val (body, bodies) = parseOneOrMore(parseTerm _)
+      val (body, bodies) = parseOneOrMore(() => parseTerm)
       assert(funDecs.size == bodies.size)
 
       if ((funDec +: funDecs).exists(_.isLeft)) {
@@ -213,8 +213,8 @@ class Parser(lexer: Lexer) extends parser.Parser(lexer) {
 
     case LT.DeclareDatatypes =>
       eat(LT.DeclareDatatypes)
-      val tps = parseMany(parseSymbol _)
-      val datatypes = parseMany(parseDatatypes _)
+      val tps = parseMany(() => parseSymbol)
+      val datatypes = parseMany(() => parseDatatypes)
       DeclareDatatypesPar(tps, datatypes)
 
     case _ => super.parseCommandWithoutParens