diff --git a/project/Build.scala b/project/Build.scala index c00065927ae55712ac33ad01111ed150c38c3fc0..11b47c4264ab690eed62d9e38ac8ebc671cc6715 100644 --- a/project/Build.scala +++ b/project/Build.scala @@ -80,6 +80,6 @@ object Leon extends Build { def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}")) lazy val bonsai = project("git://github.com/colder/bonsai.git", "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539") - lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "cdaf4707ffad39924262b91d33b660ae8d3e6471") + lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "48cec57d0a62d206ac553cb1d4a67f50fdf7dbb1") } } diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala index bce269e7a2a27b6231f96d9b2ba9f2d801f911a8..64503feee1e1322bfffa852f7a05ee134538c2d2 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala @@ -619,9 +619,9 @@ trait SMTLIBTarget { } override def check: Option[Boolean] = sendCommand(CheckSat()) match { - case CheckSatResponse(SatStatus) => Some(true) - case CheckSatResponse(UnsatStatus) => Some(false) - case CheckSatResponse(UnknownStatus) => None + case CheckSatStatus(SatStatus) => Some(true) + case CheckSatStatus(UnsatStatus) => Some(false) + case CheckSatStatus(UnknownStatus) => None case _ => None } @@ -633,7 +633,7 @@ trait SMTLIBTarget { ) - val GetValueResponse(valuationPairs) = sendCommand(cmd) + val GetValueResponseSuccess(valuationPairs) = sendCommand(cmd) valuationPairs.collect { case (SimpleSymbol(sym), value) if variables.containsB(sym) => diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala index 5eb55860c10b0d2f612561ef72513465b704ffa2..6c0e9cfbfd976274816e0dfae1bb813a641da2ef 100644 --- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala +++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3Target.scala @@ -15,7 +15,7 @@ import TreeOps.simplestValue import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, _} import _root_.smtlib.parser.Commands.{DefineSort, GetModel, DefineFun} import _root_.smtlib.interpreters.Z3Interpreter -import _root_.smtlib.parser.CommandsResponses.GetModelResponse +import _root_.smtlib.parser.CommandsResponses.GetModelResponseSuccess import _root_.smtlib.theories.Core.{Equals => SMTEquals, _} import _root_.smtlib.theories.ArraysEx @@ -171,7 +171,7 @@ trait SMTLIBZ3Target extends SMTLIBTarget { val res = sendCommand(cmd) val smodel: Seq[SExpr] = res match { - case GetModelResponse(model) => model + case GetModelResponseSuccess(model) => model case _ => Nil }