Skip to content
Snippets Groups Projects
Commit f1d7ec44 authored by Regis Blanc's avatar Regis Blanc
Browse files

update to a more robust smtlib version

parent 16278362
No related branches found
No related tags found
No related merge requests found
......@@ -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")
}
}
......@@ -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) =>
......
......@@ -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
}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment