Commit e9d94f43 authored by Christian Müller's avatar Christian Müller

add domain

parent 4fd2794e
...@@ -271,6 +271,8 @@ object toZ3 extends LazyLogging { ...@@ -271,6 +271,8 @@ object toZ3 extends LazyLogging {
sb ++= "Evaluations:\n" sb ++= "Evaluations:\n"
val sorted = model.getFuncDecls().sortBy(_.getName.toString()) val sorted = model.getFuncDecls().sortBy(_.getName.toString())
for (f <- sorted) { for (f <- sorted) {
sb ++= f.getName + f.getDomain.mkString("(",", ",")") + "\n"
val interp = model.getFuncInterp(f) val interp = model.getFuncInterp(f)
val entries = interp.getEntries val entries = interp.getEntries
for (e <- entries) { for (e <- entries) {
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment