Code Monkey home page Code Monkey logo

inox's Introduction

Inox Build Status

Inox is a solver for higher-order functional programs which provides first-class support for features such as:

  • Recursive and first-class functions
  • ADTs, integers, bitvectors, strings, set-multiset-map abstractions
  • Quantifiers
  • ADT invariants
  • Dependent types

Interfacing with the solver can take place through the Scala API by constructing the AST corresponding to the query of interest and then feeding it to one of the solvers. For more information, see:

  • The usage tutorial gives some insight on how to use Inox as a library.
  • The tree interpolators provide easy tree construction/extraction for library use.
  • A more detailed description of the available solver/evaluator API calls.
  • A description of the trees API and how to extend them.

Add Inox as a dependency

To add Inox as a dependency of your project, add the following lines to your build.sbt, where VERSION can be replaced by a tag (eg. v1.1.5), a branch name (eg. master) or a commit hash (eg. 6dfb351eee).

resolvers += "jitpack" at "https://jitpack.io"
resolvers += "uuverifiers" at "http://logicrunch.it.uu.se:4096/~wv/maven"

libraryDependencies += "com.github.epfl-lara" % "inox" % "VERSION"

Please see the releases page for the latest Inox release.

Use without the jitpack.io resolver

Alternatively, one can depend on Inox without using the jitpack.io resolver in the following way:

resolvers += "uuverifiers" at "http://logicrunch.it.uu.se:4096/~wv/maven"

def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))

lazy val inox = ghProject(
  "https://github.com/epfl-lara/inox.git",
  "6dfb351eeee44a3f13152bf510aceba7936d0e4d"
)

Command-line Interface

One can also use Inox through command-line by using the TIP format to describe the relevant query. The easiest way to use the Inox command line is to simply build the project and use the generated script.

Solver Backends

Inox relies on SMT solvers to solve the constraints it generates. Inox ships with the JVM SMT solver Princess which should work out of the box on any system.

You can also use the following external SMT solvers:

Solver binaries that you install should match your operating system and your architecture. We recommend that you install these solvers as a binary and have their binaries available in the $PATH (as z3 or cvc4). Once they are installed, you can instruct Inox to use a given sequence of solvers. The more solvers you have installed, the more successful Inox might get, because solver capabilities are incomparable.

Native Z3 API

In addition to these external binaries, a native Z3 API for Linux is bundled with Inox and should work out of the box (although having an external Z3 binary is a good idea in any case). If you build yourself, the generated script should put the native API onto your classpath. Otherwise, you will have to make sure the relevant jar from "unmanaged" is on your runtime classpath.

For other platforms than Linux, you will have to recompile the native Z3 communication layer yourself; see ScalaZ3 repository for information about how to build and package the project. You will then need to copy the resulting jar into the "unmanaged" directory named "scalaz3-$os-$arch-$scalaBinaryVersion.jar" (replace the $ variables by the relevant values).

Solver Defaults

As of now the default solver is the native Z3 API. If that solver is unavailable, a series of fallbacks take place until the princess solver. You can specify which solver to use by e.g. giving the option --solvers=smt-cvc4 to use CVC4. Check the --solvers line in Inox' help.

Building Inox

Inox is probably easiest to build on Linux-like platforms, but read on regarding other platforms.

Due to its nature, this documentation section may not always be up to date; we welcome pull requests with carefully written and tested improvements to the information below.

Requirements:

Linux & Mac OS-X

Get the sources of Inox by cloning the official Inox repository:

$ git clone https://github.com/epfl-lara/inox.git
Cloning into 'inox'...
// ...
$ cd inox
$ sbt clean compile
// takes about 1 minutes

Inox compilation generates an inox bash script that runs Inox with all the appropriate settings. This script expects argument files in the TIP input format and will report SAT or UNSAT to the specified properties.

See ./inox --help for more information about script usage.

Windows

Not yet tested!

You will need a Git shell for windows, e.g. Git for Windows. Building then proceeds as described above.

You will then need to either port the bash inox script to Windows, or run it under Cygwin.

You may be able to obtain additional tips on getting Inox to work on Windows from Mikael Mayer or on his dedicated web page.

Running Tests

Inox comes with a test suite. Consider running the following commands to invoke different test suites:

$ sbt test
$ sbt it:test

inox's People

Contributors

colder avatar dotta avatar dragos avatar earldouglas avatar gsps avatar ikuraj avatar jad-hamza avatar koksal avatar larsrh avatar manoskouk avatar mantognini avatar mario-bucev avatar mbovel avatar mikaelmayer avatar musically-ut avatar nano-o avatar psuter avatar ravimad avatar redelmann avatar regb avatar romac avatar rpiskac avatar samarion avatar samuelchassot avatar samuelgruetter avatar sstucki avatar sumith1896 avatar tihomirg avatar vkuncak avatar yannbolliger avatar

Stargazers

avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar

Watchers

avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar avatar

Forkers

ptrbman pruemmer romac jad-hamza ravimad dennisvdb namin frostweeds dragos manoskouk ostevan saraswat yannbolliger mario-bucev mbovel drganam fengwz17 samuelchassot sankalpgambhir

inox's Issues

Type error in tip printed from Stainless

In a verification condition on the Stainless side, I have a term that contains this:

if (thiss.order.leq(thiss.array((n - 1))._1, elemRef(0)._1)) {
  Return[(Boolean, SortedArray[K, T], Array[(K, T)]), Unit]((false, thiss, elemRef))
} else {
  Proceed[(Boolean, SortedArray[K, T], Array[(K, T)]), Unit](())
}

After using --debug=tip, we get a tip file where the type instantiations on Return and Proceed are lost, so Inox understands the expression in the tip file as (and this leads to a type error):

if (thiss!108.order!107.leq!6(thiss!108.array!122.arr!2((n!29 - 1))._1!0, elemRef!41.arr!2(0)._1!0)) {
  Return!1[tuple3!0[Boolean, SortedArray!5[K!37, T!91], array!118[tuple2!0[K!37, T!91]]], Cur!0](tuple3!1[Boolean, SortedArray!5[K!37, T!91], array!118[tuple2!0[K!37, T!91]]](false, thiss!108, elemRef!41))
} else {
  Proceed!1[Ret!0, Unit!1](Unit!3)
}

Can we add the type instantiations (with _) in Printer.scala? (If so, what term should I use?) Can Inox parse it back?

Using Inox in my own project

After having sbt package publish-local Inox, I naively add the following line to my build.sbt:

libraryDependencies += "ch.epfl.lara" %% "inox" % "1.0"

sbt then complains that `princess#princess_2.11;2016-07-01`` is unavailable.

Shouldn't Inox install its hand-managed dependencies ?
Is there an easy way to publish the hand-managed dependencies locally ?

Readme says Leon

The readme says Leon still. The content also does not seem any different at 1st glance.

wrong answer on higher-order problem

Inox reports a wrong answer on the following problem. The problem is about synthesizing a function f and an initial accumulator acc such that List.fold f acc that can discriminate between some lists.

inox foo.smt2 --checkmodels
[Warning ] - Model leads to runtime error: Forall model check failed
[ Error ] Something went wrong. The model should have been valid, yet we got this: Map() for formula a0 ≠ a1 && ∀x: acc. (x == a0 || x == a1) && ¬¬(fold(acc_init, l0) ≠ fold(acc_init, l1) && fold(acc_init, l2) ≠ fold(acc_init, l3))
[ Info ] => UNKNOWN

; SAT

; distinguish between lists of booleans using only `fold`
; the solver must synthesize a function and an initial accumulator

(declare-datatypes () ((nat (s (select_s_0 nat))
                            (z))))

(declare-datatypes
   ()
   ((list (cons (select_cons_0 Bool) (select_cons_1 list)) (nil))))

(declare-sort acc 0)
(declare-fun acc_init () acc)
(declare-fun f (acc Bool) acc)

; force card(acc) to be 2
(declare-fun a0 () acc)
(declare-fun a1 () acc)

(assert (not (= a0 a1)))
(assert (forall ((x acc)) (or (= x a0) (= x a1))))

(define-fun-rec
  fold
    ((a acc) (l list)) acc
    (match l
      (case nil a)
      (case (cons x tail)
        (let ((a2 (f a x)))
          (fold a2 tail)))))


(define-fun l0 () list (cons false (cons false (cons true (cons false nil)))))
(define-fun l1 () list (cons false (cons true (cons false (cons false nil)))))
(define-fun l2 () list (cons false (cons false (cons false (cons false (cons true (cons false nil)))))))
(define-fun l3 () list (cons false (cons false (cons false (cons true (cons false (cons false nil)))))))

(assert-not
 (not
   (and
    (not (= (fold acc_init l0) (fold acc_init l1)))
    (not (= (fold acc_init l2) (fold acc_init l3)))
   )))

(check-sat)

Symbolic evaluator

Following the discussion in epfl-lara/stainless#104:

@jad-hamza:
For the general case with free variables, we could take inspiration from the Coq "simpl" tactic. This tactic simplifies the terms that appear in your goal (or in your premises) by applying reductions rules (beta-reduction, etc.). But it doesn't evaluate blindly, and tries to only apply reductions that make the terms more readable (and to avoid non-termination).

For instance, given the definitions in #96, plus(n,m) would not be simplified further (even though there is a valid beta-reduction rule that can be applied), but plus(S(n),m) would be simplified to S(plus(n,m)).

@samarion:
For simplifications of non-ground terms, I also agree with @jad-hamza. Note that Inox actually already does this pretty extensively in SimplifierWithPC. However, no beta-reduction is performed for named functions, so that could be an interesting new simplification to consider. The challenge is to choose good heuristics about when a function inlining can be considered 'useful'. Possibly basing ourselves off the simp tactic could indeed be useful, but I would prefer automatic this as much as possible.

Code explosion in mergeCalls

cc: @samuelchassot

We found an example where the code simplification becomes very slow, probably due to a code explosion in mergeCalls:

// before mergeFunctions: 339 lines of code
// after liftCalls: 649 lines of code
// after mergeCalls: 30341 lines of code

Can be reproduced with the Stainless code below and the command:

stainless --watch File.scala --debug=solver,verification --functions=problem
Stainless code 
import stainless.annotation._
import stainless.collection._
import stainless.equations._
import stainless.lang._
import stainless.proof.check
import scala.annotation.tailrec
import scala.collection.immutable

object MutableLongMap {

  private final val IndexMask: Int = 0x07ffffff // = Integer.MAX_VALUE/8
  private final val MissingBit = 0x80000000
  private final val VacantBit = 0x40000000
  private final val MissVacant = 0xc0000000
  private final val EntryNotFound = 0x20000000
  private final val MAX_ITER = 2048 // arbitrary

  @mutable
  case class LongMapLongV(
      var mask: Int = IndexMask,
      var extraKeys: Int = 0,
      var zeroValue: Long = 0,
      var minValue: Long = 0,
      var _size: Int = 0,
      var _keys: Array[Long] = Array.fill(IndexMask + 1)(0),
      var _values: Array[Long] = Array.fill(IndexMask + 1)(0),
      val defaultEntry: Long => Long = (x => 0),
      var repackingKeyCount: Int = 0
  ) {

    @inline
    def valid: Boolean = {
      mask == IndexMask &&
      _values.length == mask + 1 &&
      _keys.length == _values.length &&
      mask >= 0 &&
      _size >= 0 &&
      _size < mask + 1 &&
      size >= _size &&
      extraKeys >= 0 &&
      extraKeys <= 3 &&
      arrayCountValidKeysTailRec(_keys, 0, _keys.length) == _size

    }

    @inline
    def inRange(i: Int): Boolean = {
      i >= 0 && i < mask + 1
    }

    @inline
    def validKeyIndex(k: Long, i: Int): Boolean = {
      require(valid)
      if (inRange(i)) _keys(i) == k else false
    }

    @inline
    def validZeroKeyIndex(i: Int): Boolean = {
      require(valid && inRange(i))
      inRange(i) && _keys(i) == 0
    }

    def size: Int = {
      _size + (extraKeys + 1) / 2
    }

    def isEmpty: Boolean = {
      require(valid)
      _size == 0
    }.ensuring(_ => valid)

    private def toIndex(k: Long): Int = {
      require(valid)
      val h = ((k ^ (k >>> 32)) & 0xffffffffL).toInt
      val x = (h ^ (h >>> 16)) * 0x85ebca6b
      (x ^ (x >>> 13)) & mask
    }.ensuring(res => valid && res < _keys.length)

    @inline
    def getCurrentListMap(from: Int): ListMapLongKey[Long] = {
      require(valid && from >= 0 && from <= _keys.length)

      val res = if ((extraKeys & 1) != 0 && (extraKeys & 2) != 0) {
        (getCurrentListMapNoExtraKeys(from) + (0L, zeroValue)) + (Long.MinValue, minValue)
      } else if ((extraKeys & 1) != 0 && (extraKeys & 2) == 0) {
        getCurrentListMapNoExtraKeys(from) + (0L, zeroValue)
      } else if ((extraKeys & 2) != 0 && (extraKeys & 1) == 0) {
        getCurrentListMapNoExtraKeys(from) + (Long.MinValue, minValue)
      } else {
        getCurrentListMapNoExtraKeys(from)
      }
      if (from < _keys.length && validKeyInArray(_keys(from))) {
        ListMapLongKeyLemmas.addStillContains(getCurrentListMapNoExtraKeys(from), 0, zeroValue, _keys(from))
        ListMapLongKeyLemmas.addStillContains(getCurrentListMapNoExtraKeys(from), Long.MinValue, minValue, _keys(from))
        ListMapLongKeyLemmas.addApplyDifferent(getCurrentListMapNoExtraKeys(from), 0, zeroValue, _keys(from))
        ListMapLongKeyLemmas.addApplyDifferent(getCurrentListMapNoExtraKeys(from), Long.MinValue, minValue, _keys(from))
      }

      res

    }.ensuring(res =>
      valid &&
        (if (from < _keys.length && validKeyInArray(_keys(from))) res.contains(_keys(from)) && res(_keys(from)) == _values(from) else true) &&
        (if ((extraKeys & 1) != 0) res.contains(0) && res(0) == zeroValue else !res.contains(0)) &&
        (if ((extraKeys & 2) != 0) res.contains(Long.MinValue) && res(Long.MinValue) == minValue else !res.contains(Long.MinValue))
    )

    def getCurrentListMapNoExtraKeys(from: Int): ListMapLongKey[Long] = {
      require(valid && from >= 0 && from <= _keys.length)
      decreases(_keys.length + 1 -from)
      if (from >= _keys.length) {
        ListMapLongKey.empty[Long]
      } else if (validKeyInArray(_keys(from))) {
        ListMapLongKeyLemmas.addStillNotContains(getCurrentListMapNoExtraKeys(from + 1), _keys(from), _values(from), 0)

        getCurrentListMapNoExtraKeys(from + 1) + (_keys(from), _values(from))
      } else {
        getCurrentListMapNoExtraKeys(from + 1)
      }
    }.ensuring(res => valid &&
      !res.contains(0) && !res.contains(Long.MinValue) &&
        (if (from < _keys.length && validKeyInArray(_keys(from)))
           res.contains(_keys(from)) && res(_keys(from)) == _values(from)
         else if (from < _keys.length) res == getCurrentListMapNoExtraKeys(from + 1)
         else res.isEmpty)
    )

    @pure
    def problem(): Unit = {
      require(valid)
      val from = 0
      val res = getCurrentListMap(from)
    }.ensuring(_ => valid && (if ((extraKeys & 1) != 0) getCurrentListMap(0).contains(0) else !getCurrentListMap(0).contains(0)))

  }

  @extern
  def assume(b: Boolean): Unit = {}.ensuring(_ => b)

  @inline
  def validKeyInArray(l: Long): Boolean = {
    l != 0 && l != Long.MinValue
  }

  @tailrec
  @pure
  def arrayCountValidKeysTailRec(
      a: Array[Long],
      from: Int,
      to: Int
  ): Int = {
    require(
      from <= to && from >= 0 && to <= a.length && a.length < Integer.MAX_VALUE
    )
    decreases(a.length-from)
    if (from >= to) {
      0
    } else {
      if (validKeyInArray(a(from))) {
        1 + arrayCountValidKeysTailRec(a, from + 1, to)
      } else {
        arrayCountValidKeysTailRec(a, from + 1, to)
      }
    }
  }.ensuring(res => res >= 0 && res <= a.length - from)


}

case class ListMapLongKey[B](toList: List[(Long, B)]) {
  require(TupleListOps.isStrictlySorted(toList))

  @inline
  def isEmpty: Boolean = toList.isEmpty
  @inline
  def head: (Long, B) = {
    require(!isEmpty)
    toList.head
  }
  @inline
  def tail: ListMapLongKey[B] = {
    require(!isEmpty)
    ListMapLongKey(toList.tail)
  }

  @inlineOnce @extern
  def contains(key: Long): Boolean = {
    TupleListOps.containsKey(toList, key)

  }.ensuring(res => !res || this.get(key).isDefined)

  @inline
  def get(key: Long): Option[B] = {
    TupleListOps.getValueByKey(toList, key)
  }
  @inline
  def keysOf(value: B): List[Long] = {
    TupleListOps.getKeysOf(toList, value)
  }
  @inline
  def apply(key: Long): B = {
    require(contains(key))
    get(key).get
  }

  @inline
  def +(keyValue: (Long, B)): ListMapLongKey[B] = {

    val newList = TupleListOps.insertStrictlySorted(toList, keyValue._1, keyValue._2)

    ListMapLongKey(newList)

  }.ensuring(res => res.contains(keyValue._1) && res.get(keyValue._1) == Some(keyValue._2))

  // @inlineOnce
  def ++(keyValues: List[(Long, B)]): ListMapLongKey[B] = {
    decreases(keyValues)
    keyValues match {
      case Nil()                => this
      case Cons(keyValue, rest) => (this + keyValue) ++ rest
    }
  }
  // @inlineOnce
  def -(key: Long): ListMapLongKey[B] = {
    ListMapLongKey(TupleListOps.removeStrictlySorted(toList, key))
  }.ensuring(res => !res.contains(key))

  // @inlineOnce
  def --(keys: List[Long]): ListMapLongKey[B] = {
    decreases(keys)
    keys match {
    case Nil()           => this
    case Cons(key, rest) => (this - key) -- rest
  }
  }
  @inline
  def forall(p: ((Long, B)) => Boolean): Boolean = {
    toList.forall(p)
  }
}

object TupleListOps {

  @inline
  def invariantList[B](l: List[(Long, B)]): Boolean = {
    isStrictlySorted(l)
  }

  @extern
  def getKeysOf[B](l: List[(Long, B)], value: B): List[Long] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._2 == value) => {
        head._1 :: getKeysOf(tl, value)
      }
      case head :: tl if (head._2 != value) => {
        val r = getKeysOf(tl, value)
        getKeysOf(tl, value)
      }
      case Nil() => Nil[Long]()
    }

  }.ensuring(res => res.forall(getValueByKey(l, _) == Some(value)))

  def getValueByKey[B](l: List[(Long, B)], key: Long): Option[B] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._1 == key) => Some(head._2)
      case head :: tl if (head._1 != key) => getValueByKey(tl, key)
      case Nil()                          => None[B]
    }

  }

  def insertStrictlySorted[B](l: List[(Long, B)], newKey: Long, newValue: B): List[(Long, B)] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._1 < newKey)  => head :: insertStrictlySorted(tl, newKey, newValue)
      case head :: tl if (head._1 == newKey) => (newKey, newValue) :: tl
      case head :: tl if (head._1 > newKey)  => (newKey, newValue) :: head :: tl
      case Nil()                             => (newKey, newValue) :: Nil()
    }
  }.ensuring(res => invariantList(res) && containsKey(res, newKey) && res.contains((newKey, newValue)))

  def removeStrictlySorted[B](l: List[(Long, B)], key: Long): List[(Long, B)] = {
    require(invariantList(l))
    decreases(l)

    l match {
      case head :: tl if (head._1 == key) => tl
      case head :: tl if (head._1 != key) => head :: removeStrictlySorted(tl, key)
      case Nil()                          => Nil[(Long, B)]()
    }
  }.ensuring(res => invariantList(res) && !containsKey(res, key))


  def isStrictlySorted[B](l: List[(Long, B)]): Boolean = {
    decreases(l)
    l match {
      case Nil()                                     => true
      case Cons(_, Nil())                            => true
      case Cons(h1, Cons(h2, _)) if (h1._1 >= h2._1) => false
      case Cons(_, t)                                => isStrictlySorted(t)
    }
  }

  def containsKey[B](l: List[(Long, B)], key: Long): Boolean = {
    require(invariantList(l))
    decreases(l)
    l match {
      case head :: tl if(head._1 == key) => true
      case head :: tl if(head._1 > key) => false
      case head :: tl if(head._1 < key) => containsKey(tl, key)
      case Nil() => false

    }
  }
}

object ListMapLongKey {
  def empty[B]: ListMapLongKey[B] = ListMapLongKey[B](List.empty[(Long, B)])
}

object ListMapLongKeyLemmas {
  import ListSpecs._

  @opaque
  def addValidProp[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, a: Long, b: B): Unit = {
    require(lm.forall(p) && p(a, b))
    decreases(lm.toList.size)

    if (!lm.isEmpty)
      addValidProp(lm.tail, p, a, b)

  }.ensuring { _ =>
    val nlm = lm + (a, b)
    nlm.forall(p)
  }

  @opaque
  def removeValidProp[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, a: Long): Unit = {
    require(lm.forall(p))
    decreases(lm.toList.size)
    if (!lm.isEmpty)
      removeValidProp(lm.tail, p, a)

  }.ensuring { _ =>
    val nlm = lm - a
    nlm.forall(p)
  }

  @opaque
  def insertAllValidProp[B](lm: ListMapLongKey[B], kvs: List[(Long, B)], p: ((Long, B)) => Boolean): Unit = {
    require(lm.forall(p) && kvs.forall(p))
    decreases(kvs)

    if (!kvs.isEmpty) {
      addValidProp(lm, p, kvs.head._1, kvs.head._2)
      insertAllValidProp(lm + kvs.head, kvs.tail, p)
    }

  }.ensuring { _ =>
    val nlm = lm ++ kvs
    nlm.forall(p)
  }

  @opaque
  def removeAllValidProp[B](lm: ListMapLongKey[B], l: List[Long], p: ((Long, B)) => Boolean): Unit = {
    require(lm.forall(p))
    decreases(l)

    if (!l.isEmpty) {
      removeValidProp(lm, p, l.head)
      removeAllValidProp(lm - l.head, l.tail, p)
    }

  }.ensuring { _ =>
    val nlm = lm -- l
    nlm.forall(p)
  }

  @opaque @extern
  def addApplyDifferent[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
    require(lm.contains(a0) && a0 != a)

  }.ensuring(_ => (lm + (a -> b))(a0) == lm(a0))

  @opaque @extern
  def addStillContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
    require(lm.contains(a0))

  }.ensuring(_ => (lm + (a, b)).contains(a0))

  @opaque @extern
  def addStillNotContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
    require(!lm.contains(a0) && a != a0)

  }.ensuring(_ => !(lm + (a, b)).contains(a0))

  @opaque
  def applyForall[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, k: Long): Unit = {
    require(lm.forall(p) && lm.contains(k))
    decreases(lm.toList.size)

    if (!lm.isEmpty && lm.toList.head._1 != k)
      applyForall(lm.tail, p, k)

  }.ensuring(_ => p(k, lm(k)))

  @opaque
  def getForall[B](lm: ListMapLongKey[B], p: ((Long, B)) => Boolean, k: Long): Unit = {
    require(lm.forall(p))
    decreases(lm.toList.size)

    if (!lm.isEmpty && lm.toList.head._1 != k)
      getForall(lm.tail, p, k)

  }.ensuring(_ => lm.get(k).forall(v => p(k, v)))

  @opaque
  def uniqueImage[B](lm: ListMapLongKey[B], a: Long, b: B): Unit = {
    require(lm.toList.contains((a, b)))

  }.ensuring(_ => lm.get(a) == Some[B](b))

  @opaque
  def keysOfSound[B](lm: ListMapLongKey[B], value: B): Unit = {
  }.ensuring(_ => lm.keysOf(value).forall(key => lm.get(key) == Some[B](value)))
}
Expression before mergeFunctions 
¬(thiss.mask ≠ IndexMask || thiss._values.size ≠ thiss.mask + 1 || thiss._keys.size ≠ thiss._values.size || thiss.mask < 0 || thiss._size < 0 || thiss._size >= thiss.mask + 1 || size(thiss) < thiss._size || thiss.extraKeys < 0 || thiss.extraKeys > 3 || arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) ≠ thiss._size || from ≠ 0 || res ≠ {
  val cond: Boolean = (thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0) && from <= thiss._keys.size
  val res: ListMapLongKey[Long] = {
    val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) ≠ 0) {
      val inlined: ListMapLongKey[Long] = {
        val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
        assume({
          val res: Boolean = choose((empty$140: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
          res
        } && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
        ListMapLongKey[Long](newList)
      }
      val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
      assume({
        val res: Boolean = choose((empty$141: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
        res
      } && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
      res
    } else if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) == 0) {
      val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
      val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
      assume({
        val res: Boolean = choose((empty$142: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
        res
      } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
      res
    } else if ((thiss.extraKeys & 2) ≠ 0 && (thiss.extraKeys & 1) == 0) {
      val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
      val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
      assume({
        val res: Boolean = choose((empty$143: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
        res
      } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
      res
    } else {
      getCurrentListMapNoExtraKeys(thiss, from)
    }
    val t: Unit = if (from < thiss._keys.size && {
      val l: Long = thiss._keys.arr(from)
      l ≠ 0.toLong && l ≠ -9223372036854775808
    }) {
      val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
      val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
      val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
      addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
    } else {
      ()
    }
    t
  }
  assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
    val l: Long = thiss._keys.arr(from)
    l ≠ 0.toLong && l ≠ -9223372036854775808
  }) || {
    val res: Boolean = choose((empty$144: Boolean) => true)
    assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
    res
  } && {
    val key: Long = thiss._keys.arr(from)
    val cond: Boolean = {
      val res: Boolean = choose((empty$145: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
      res
    }
    get[Long](getValueByKey[Long](res.toList, key))
  } == thiss._values.arr(from))) && (if ((thiss.extraKeys & 1) ≠ 0) {
    {
      val res: Boolean = choose((empty$146: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
      res
    } && {
      val key: Long = 0
      val cond: Boolean = {
        val res: Boolean = choose((empty$147: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss.zeroValue
  } else {
    val res: Boolean = choose((empty$148: Boolean) => true)
    ¬{
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
      res
    }
  })) && (if ((thiss.extraKeys & 2) ≠ 0) {
    {
      val res: Boolean = choose((empty$149: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
      res
    } && {
      val key: Long = -9223372036854775808
      val cond: Boolean = {
        val res: Boolean = choose((empty$150: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss.minValue
  } else {
    val res: Boolean = choose((empty$151: Boolean) => true)
    ¬{
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
      res
    }
  }))
  res
} || x$2 ≠ () || thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (if ((thiss.extraKeys & 1) ≠ 0) {
  val from: Int = 0
  val inlined: ListMapLongKey[Long] = {
    val t: Boolean = thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0
    val res: ListMapLongKey[Long] = {
      val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 2) ≠ 0) {
        val inlined: ListMapLongKey[Long] = {
          val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
          assume({
            val res: Boolean = choose((empty$152: Boolean) => true)
            assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
            res
          } && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
          ListMapLongKey[Long](newList)
        }
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$153: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else if ((thiss.extraKeys & 2) == 0) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
        assume({
          val res: Boolean = choose((empty$154: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
        res
      } else if (false) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$155: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else {
        getCurrentListMapNoExtraKeys(thiss, from)
      }
      val t: Unit = if (from < thiss._keys.size && {
        val l: Long = thiss._keys.arr(from)
        l ≠ 0.toLong && l ≠ -9223372036854775808
      }) {
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
        val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
      } else {
        ()
      }
      t
    }
    assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
      val l: Long = thiss._keys.arr(from)
      l ≠ 0.toLong && l ≠ -9223372036854775808
    }) || {
      val res: Boolean = choose((empty$156: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
      res
    } && {
      val key: Long = thiss._keys.arr(from)
      val cond: Boolean = {
        val res: Boolean = choose((empty$157: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss._values.arr(from))) && {
      val res: Boolean = choose((empty$158: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
      res
    } && {
      val key: Long = 0
      val cond: Boolean = {
        val res: Boolean = choose((empty$159: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss.zeroValue) && (if ((thiss.extraKeys & 2) ≠ 0) {
      {
        val res: Boolean = choose((empty$160: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      } && {
        val key: Long = -9223372036854775808
        val cond: Boolean = {
          val res: Boolean = choose((empty$161: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
          res
        }
        get[Long](getValueByKey[Long](res.toList, key))
      } == thiss.minValue
    } else {
      val res: Boolean = choose((empty$162: Boolean) => true)
      ¬{
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      }
    }))
    res
  }
  val res: Boolean = choose((empty$163: Boolean) => true)
  assume(¬res || isDefined[Long](getValueByKey[Long](inlined.toList, 0)))
  res
} else {
  val from: Int = 0
  val inlined: ListMapLongKey[Long] = {
    val t: Boolean = thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && from >= 0
    val res: ListMapLongKey[Long] = {
      val t: ListMapLongKey[Long] = if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) ≠ 0) {
        val inlined: ListMapLongKey[Long] = {
          val newList: List[(Long, Long)] = insertStrictlySorted[Long](getCurrentListMapNoExtraKeys(thiss, from).toList, 0, thiss.zeroValue)
          assume({
            val res: Boolean = choose((empty$164: Boolean) => true)
            assume(¬res || isDefined[Long](getValueByKey[Long](newList, 0)))
            res
          } && getValueByKey[Long](newList, 0) == Some[Long](thiss.zeroValue))
          ListMapLongKey[Long](newList)
        }
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$165: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](inlined.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else if ((thiss.extraKeys & 1) ≠ 0 && (thiss.extraKeys & 2) == 0) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue))
        assume({
          val res: Boolean = choose((empty$166: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, 0, thiss.zeroValue), 0) == Some[Long](thiss.zeroValue))
        res
      } else if ((thiss.extraKeys & 2) ≠ 0 && (thiss.extraKeys & 1) == 0) {
        val thiss: ListMapLongKey[Long] = getCurrentListMapNoExtraKeys(thiss, from)
        val res: ListMapLongKey[Long] = ListMapLongKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue))
        assume({
          val res: Boolean = choose((empty$167: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808)))
          res
        } && getValueByKey[Long](insertStrictlySorted[Long](thiss.toList, -9223372036854775808, thiss.minValue), -9223372036854775808) == Some[Long](thiss.minValue))
        res
      } else {
        getCurrentListMapNoExtraKeys(thiss, from)
      }
      val t: Unit = if (from < thiss._keys.size && {
        val l: Long = thiss._keys.arr(from)
        l ≠ 0.toLong && l ≠ -9223372036854775808
      }) {
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        val tmp: Unit = addStillContains[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
        val tmp: Unit = addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), 0, thiss.zeroValue, thiss._keys.arr(from))
        addApplyDifferent[Long](getCurrentListMapNoExtraKeys(thiss, from), -9223372036854775808, thiss.minValue, thiss._keys.arr(from))
      } else {
        ()
      }
      t
    }
    assume(((thiss.mask == IndexMask && thiss._values.size == thiss.mask + 1 && thiss._keys.size == thiss._values.size && thiss.mask >= 0 && thiss._size >= 0 && thiss._size < thiss.mask + 1 && size(thiss) >= thiss._size && thiss.extraKeys >= 0 && thiss.extraKeys <= 3 && arrayCountValidKeysTailRec(thiss._keys, 0, thiss._keys.size) == thiss._size && (¬(from < thiss._keys.size && {
      val l: Long = thiss._keys.arr(from)
      l ≠ 0.toLong && l ≠ -9223372036854775808
    }) || {
      val res: Boolean = choose((empty$168: Boolean) => true)
      assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, thiss._keys.arr(from))))
      res
    } && {
      val key: Long = thiss._keys.arr(from)
      val cond: Boolean = {
        val res: Boolean = choose((empty$169: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
        res
      }
      get[Long](getValueByKey[Long](res.toList, key))
    } == thiss._values.arr(from))) && (if ((thiss.extraKeys & 1) ≠ 0) {
      {
        val res: Boolean = choose((empty$170: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
        res
      } && {
        val key: Long = 0
        val cond: Boolean = {
          val res: Boolean = choose((empty$171: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
          res
        }
        get[Long](getValueByKey[Long](res.toList, key))
      } == thiss.zeroValue
    } else {
      val res: Boolean = choose((empty$172: Boolean) => true)
      ¬{
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, 0)))
        res
      }
    })) && (if ((thiss.extraKeys & 2) ≠ 0) {
      {
        val res: Boolean = choose((empty$173: Boolean) => true)
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      } && {
        val key: Long = -9223372036854775808
        val cond: Boolean = {
          val res: Boolean = choose((empty$174: Boolean) => true)
          assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, key)))
          res
        }
        get[Long](getValueByKey[Long](res.toList, key))
      } == thiss.minValue
    } else {
      val res: Boolean = choose((empty$175: Boolean) => true)
      ¬{
        assume(¬res || isDefined[Long](getValueByKey[Long](res.toList, -9223372036854775808)))
        res
      }
    }))
    res
  }
  val res: Boolean = choose((empty$176: Boolean) => true)
  ¬{
    assume(¬res || isDefined[Long](getValueByKey[Long](inlined.toList, 0)))
    res
  }
}))

"String index out of range: 0" in ASCIIStringEncoder

Stainless throws this exception when running the termination checker (stainless --solvers=nativez3 --termination) over this benchmark:

import stainless.lang._
import stainless.annotation._
import stainless.collection._

object index {
  val xs = List("a" -> 1, "b" -> 2, "c" -> 3, "d" -> 4)

  def test(map: Map[String, Int]) = {
    val res = xs.foldLeft(map) {
      case (acc, (k, v)) => acc.updated(k, v)
    }

    res.get("d") == Some(4)
  }.holds
}

The string it is apparently attempting unescape is: !0!

Trace: (click to expand) 
[Internal] Error: String index out of range: 0. Trace:
[Internal] - java.lang.String.charAt(String.java:658)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$class.inox$solvers$theories$ASCIIStringEncoder$$decodeFirstByte(ASCIIStringEncoder.scala:51)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:89)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:103)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:106)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:153)
[Internal] - inox.ast.TreeTransformer$$anonfun$4.apply(TreeOps.scala:152)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - inox.ast.TreeTransformer$class.transform(TreeOps.scala:152)
[Internal] - inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:119)
[Internal] - inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:274)
[Internal] - inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:293)
[Internal] - inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27)
[Internal] - inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:65)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.decode(SolverFactory.scala:122)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:541)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:541)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:179)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.Map$Map3.foreach(Map.scala:161)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:179)
[Internal] - inox.solvers.z3.Z3Unrolling$ModelWrapper.getModel(Z3Unrolling.scala:66)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:541)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:671)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:552)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:552)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:122)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$checkAssumptions$1.apply(TimeoutSolver.scala:44)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$checkAssumptions$1.apply(TimeoutSolver.scala:44)
[Internal] - inox.utils.TimeoutFor.interruptAfter(TimeoutFor.scala:36)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:43)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:122)
[Internal] - inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:61)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.checkAssumptions(SolverFactory.scala:122)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:88)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:122)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$check$1.apply(TimeoutSolver.scala:32)
[Internal] - inox.solvers.combinators.TimeoutSolver$$anonfun$check$1.apply(TimeoutSolver.scala:32)
[Internal] - inox.utils.TimeoutFor.interruptAfter(TimeoutFor.scala:36)
[Internal] - inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:31)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:122)
[Internal] - inox.tip.TipDebugger$class.check(TipDebugger.scala:56)
[Internal] - inox.solvers.SolverFactory$$anonfun$getFromName$1$$anon$6.check(SolverFactory.scala:122)
[Internal] - inox.solvers.SimpleSolverAPI$class.solveVALID(SimpleSolverAPI.scala:22)
[Internal] - inox.solvers.SimpleSolverAPI$$anon$1.solveVALID(SimpleSolverAPI.scala:57)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7$$anonfun$8.apply(RelationProcessor.scala:46)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7$$anonfun$8.apply(RelationProcessor.scala:45)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.Set$Set2.foreach(Set.scala:128)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:47)
[Internal] - scala.collection.SetLike$class.map(SetLike.scala:92)
[Internal] - scala.collection.AbstractSet.map(Set.scala:47)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7.apply(RelationProcessor.scala:45)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1$$anonfun$7.apply(RelationProcessor.scala:44)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.mutable.ResizableArray$class.foreach(ResizableArray.scala:59)
[Internal] - scala.collection.mutable.ArrayBuffer.foreach(ArrayBuffer.scala:48)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.AbstractTraversable.map(Traversable.scala:104)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1.apply(RelationProcessor.scala:44)
[Internal] - stainless.termination.RelationProcessor$$anonfun$run$1.apply(RelationProcessor.scala:21)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - stainless.termination.RelationProcessor$class.run(RelationProcessor.scala:21)
[Internal] - stainless.termination.TerminationChecker$$anon$1$lexicographicProcessor$.run(TerminationChecker.scala:110)
[Internal] - stainless.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:204)
[Internal] - stainless.termination.ProcessingPipeline$$anon$1.next(ProcessingPipeline.scala:197)
[Internal] - scala.collection.Iterator$$anon$13.hasNext(Iterator.scala:462)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - stainless.termination.ProcessingPipeline$class.runPipeline(ProcessingPipeline.scala:232)
[Internal] - stainless.termination.ProcessingPipeline$class.terminates(ProcessingPipeline.scala:156)
[Internal] - stainless.termination.TerminationChecker$$anon$1.terminates(TerminationChecker.scala:39)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2$$anonfun$3.apply(TerminationComponent.scala:60)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2$$anonfun$3.apply(TerminationComponent.scala:60)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2.apply(TerminationComponent.scala:60)
[Internal] - stainless.termination.TerminationComponent$$anonfun$2.apply(TerminationComponent.scala:59)
[Internal] - scala.collection.immutable.Stream$$anonfun$map$1.apply(Stream.scala:418)
[Internal] - scala.collection.immutable.Stream$$anonfun$map$1.apply(Stream.scala:418)
[Internal] - scala.collection.immutable.Stream$Cons.tail(Stream.scala:1233)
[Internal] - scala.collection.immutable.Stream$Cons.tail(Stream.scala:1223)
[Internal] - scala.collection.immutable.Stream.foreach(Stream.scala:595)
[Internal] - scala.collection.TraversableOnce$class.toMap(TraversableOnce.scala:316)
[Internal] - scala.collection.AbstractTraversable.toMap(Traversable.scala:104)
[Internal] - stainless.termination.TerminationComponent$$anon$2.<init>(TerminationComponent.scala:69)
[Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:67)
[Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8)
[Internal] - stainless.SimpleComponent$class.apply(Component.scala:87)
[Internal] - stainless.termination.TerminationComponent$.apply(TerminationComponent.scala:8)
[Internal] - stainless.termination.TerminationCallBack.solve(TerminationCallBack.scala:28)
[Internal] - stainless.termination.TerminationCallBack.solve(TerminationCallBack.scala:12)
[Internal] - stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:191)
[Internal] - stainless.frontend.CallBackWithRegistry$$anon$2.call(CallBackWithRegistry.scala:190)
[Internal] - java.util.concurrent.FutureTask.run(FutureTask.java:266)
[Internal] - java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
[Internal] - java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
[Internal] - java.lang.Thread.run(Thread.java:748)

MatchError: String in SMTLIBTarget

I don't know how to solve this. I don't know why there is a pattern matching error - I checked in the source, and there is nothing but a basic pattern matching on "Implies", which if it failed, should move on to the next one. I'm using inox 1.0.1 for scala 2.11

Can you please help me with that?

scala.MatchError: String (of class inox.ast.Types$ADTType)
[info]   at inox.solvers.smtlib.SMTLIBTarget$class.toSMT(SMTLIBTarget.scala:356)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.inox$solvers$smtlib$Z3Target$$super$toSMT(SolverFactory.scala:176)
[info]   at inox.solvers.smtlib.Z3Target$class.toSMT(Z3Target.scala:212)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.toSMT(SolverFactory.scala:176)
[info]   at inox.solvers.smtlib.SMTLIBTarget$class.toSMT(SMTLIBTarget.scala:354)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.inox$solvers$smtlib$Z3Target$$super$toSMT(SolverFactory.scala:176)
[info]   at inox.solvers.smtlib.Z3Target$class.toSMT(Z3Target.scala:212)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$3$$anon$3$underlying$.toSMT(SolverFactory.scala:176)
[info]   at inox.solvers.smtlib.SMTLIBTarget$$anonfun$toSMT$8.apply(SMTLIBTarget.scala:428)
[info]   at inox.solvers.smtlib.SMTLIBTarget$$anonfun$toSMT$8.apply(SMTLIBTarget.scala:428)

Missing support for str.++

This happened in Stainless in PR epfl-lara/stainless#1016 in CodeGenVerificationSuite on InnerClasses5

72: verification/valid/InnerClasses5 type-checker=false codegen *** FAILED *** (567 milliseconds)
[info]   inox.package$FatalError: Missfomed SMT source in (str.++ (seq.unit #x54) (seq.unit #x54) (seq.unit #x65) (seq.unit #x65) (seq.unit #x73) (seq.unit #x73) (seq.unit #x74) (seq.unit #x74)):
[info] Unknown SMT term of class: class smtlib.trees.Terms$FunctionApplication

Error in documentation when executing `sbt compile`

I'm getting the following error when running sbt compile on Inox:

[info] Compiling 158 Scala sources to ~/inox/target/scala-2.12/classes ...
[info] Done compiling.
[info] Running (fork) tut.TutMain ~/inox/src/main/doc/trees.md ~/inox/doc .*\.(md|markdown|txt|htm|html) -deprecation -unchecked -feature
[info] [tut] compiling: ~/inox/src/main/doc/trees.md
[info] Running (fork) tut.TutMain ~/inox/src/main/doc/interpolations.md ~/inox/doc .*\.(md|markdown|txt|htm|html) -deprecation -unchecked -feature
[info] [tut] compiling: ~/inox/src/main/doc/interpolations.md
[error] Exception in thread "main" scala.reflect.internal.Symbols$CyclicReference: illegal cyclic reference involving <refinement of inox.ast.SimpleSymbols with inox.ast.Trees>
[error] java.lang.RuntimeException: Nonzero exit code returned from runner: 1
[error]         at scala.sys.package$.error(package.scala:26)
[error]         at tut.TutPlugin$.$anonfun$tutOne$1(TutPlugin.scala:149)
[error]         at scala.util.Success.foreach(Try.scala:249)
[error]         at tut.TutPlugin$.tutOne(TutPlugin.scala:149)
[error]         at tut.TutPlugin$.$anonfun$tutAll$1(TutPlugin.scala:157)
[error]         at scala.collection.immutable.List.flatMap(List.scala:334)
[error]         at tut.TutPlugin$.tutAll(TutPlugin.scala:157)
[error]         at tut.TutPlugin$.handleUpdate$1(TutPlugin.scala:106)
[error]         at tut.TutPlugin$.$anonfun$projectSettings$29(TutPlugin.scala:111)
[error]         at sbt.util.FileFunction$.$anonfun$cached$4(FileFunction.scala:147)
[error]         at sbt.util.Difference.apply(Tracked.scala:313)
[error]         at sbt.util.Difference.apply(Tracked.scala:293)
[error]         at sbt.util.FileFunction$.$anonfun$cached$3(FileFunction.scala:143)
[error]         at sbt.util.Difference.apply(Tracked.scala:313)
[error]         at sbt.util.Difference.apply(Tracked.scala:288)
[error]         at sbt.util.FileFunction$.$anonfun$cached$2(FileFunction.scala:142)
[error]         at tut.TutPlugin$.$anonfun$projectSettings$25(TutPlugin.scala:111)
[error]         at scala.Function1.$anonfun$compose$1(Function1.scala:44)
[error]         at sbt.internal.util.$tilde$greater.$anonfun$$u2219$1(TypeFunctions.scala:40)
[error]         at sbt.std.Transform$$anon$4.work(System.scala:67)
[error]         at sbt.Execute.$anonfun$submit$2(Execute.scala:269)
[error]         at sbt.internal.util.ErrorHandling$.wideConvert(ErrorHandling.scala:16)
[error]         at sbt.Execute.work(Execute.scala:278)
[error]         at sbt.Execute.$anonfun$submit$1(Execute.scala:269)
[error]         at sbt.ConcurrentRestrictions$$anon$4.$anonfun$submitValid$1(ConcurrentRestrictions.scala:178)
[error]         at sbt.CompletionService$$anon$2.call(CompletionService.scala:37)
[error]         at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[error]         at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
[error]         at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[error]         at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
[error]         at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
[error]         at java.lang.Thread.run(Thread.java:748)
[error] (tutQuick) Nonzero exit code returned from runner: 1

RecursiveEvaluator is wrong for Application

Test case:

import inox._
import inox.trees._
import inox.trees.dsl._
import inox.evaluators.EvaluationResults

val ap = ValDef(FreshIdentifier("a"), StringType, Set())
val bp = ValDef(FreshIdentifier("b"), StringType, Set())

val body = 
  Application(
    Application(
    Lambda(Seq(ap),
      Lambda(Seq(bp),
        StringConcat(StringConcat(ap.toVariable, StringLiteral(":")), bp.toVariable)
      )
    ), Seq(StringLiteral("Winner"))), Seq(StringLiteral("Mikael")))

val main = FreshIdentifier("main")
val funDef = mkFunDef(main)()(_ => (Seq(), StringType, _ => body))

val prog = InoxProgram(
  Context.empty,
  funDef::Nil, List()
)

prog.getEvaluator.eval(FunctionInvocation(main, Seq(), Seq())) match {
  case EvaluationResults.Successful(e) => println(e);e
}

Run and you get:

"Winner:Winner:"

instead of

"Winner:Mikael"

Inox fails to build because of sbt-tut

On latest master (3c23a86), running sbt clean compile yields the following error:

[info] [tut] compiling: /Users/romac/Code/@epfl-lara/inox/src/main/doc/tutorial.md
[error] Exception in thread "main" scala.reflect.internal.Symbols$CyclicReference: illegal cyclic reference involving <refinement of inox.ast.SimpleSym

cons instead of list in the tutorial?

Hello,
Is this an issue? In the tutorial, you say for the size funciton

if_ (ls.isInstOf(T(list)(tp))) {
  ... /* `1 + size(ls.tail)` */
} else_ {
  ... /* 0 */
}

But instead of list, shouldn't it be cons?
Especially in the remaining, there is no more reference to the consConstructor or cons anymore.

/* The `E(BigInt(i))` calls correspond to `IntegerLiteral(i)` ASTs. */
if_ (ls.isInstOf(T(list)(tp))) {
  /* The recursive call to `size` written `E(size)(tp)(...)` corresponds to
   * the AST `FunctionInvocation(size, Seq(tp), Seq(...))`.
   * Note that we refer to the symbol `tail` of the `consConstructor`'s second
   * field when building the selector AST. */
  E(BigInt(1)) + E(size)(tp)(ls.asInstOf(T(list)(tp)).getField(tail))
} else_ {
  E(BigInt(0))
}

If this is perfectly valid, can you explain me why and maybe I will update the tutorial to reflect that.

Test suite fails with Z3 4.6

The inox test suite fails when run against Z3 4.6, as it seems like Z3 now requires explicitly enabling unsat assumption construction.

For instance:

[info] - 158: simple theorem solvr=smt-z3 lucky=true check=true assum=true assck=false model=1 *** FAILED *** (39 milliseconds)
[info]   inox.package$FatalError: Unexpected error from z3 solver: line 22 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)

Tests failing with Z3 4.6.0 or newer

Tests are currently not going through for me on master with Z3 4.6.0 or Z3 4.7.1. With Z3 4.5.0 they're ok. (different error than #57)

[info] - 133: size(x) > 0 is satisfiable solvr=smt-z3 lucky=false check=false assum=true assck=false model=0 *** FAILED *** (27 milliseconds)
[info]   inox.package$FatalError: Unexpected error from z3 solver: Solver encountered exception: smtlib.parser.Parser$UnexpectedTokenException: Unexpected token at position: (15, 2). Expected: [SymbolLitKind]. Found: OParen

Key not found exception on Stainless test case with extern method with quantifiers

The following Stainless testcase crashes both Inox master and latest release with a key not found exception. Check the comments for a few variants which do not crash Inox (but yield invalid models).

import stainless.lang._
import stainless.annotation._

object SetMapExternBug {

  @extern // Without @extern: OK but invalid model
  def map(set: Set[BigInt])(f: BigInt => BigInt): Set[BigInt] = {
    (??? : Set[BigInt])
  } ensuring { res =>
    forall((a: BigInt) => set.contains(a) == res.contains(f(a)))
  }

  def test(set: Set[BigInt]) = {
    require(set == Set[BigInt](1, 2))

    // val res = map(set)(x => x) // OK but invalid model

    val res = map(map(set)(x => x))(x => x) // CRASH

    assert(res == set)
  }
}

Here is the TIP for the VC, which when fed to Inox CLI, does not output anything.

(declare-const set!1 (Set Int))

(define-fun map!6 ((set!0 (Set Int)) (f!30 (=> Int Int))) (Set Int) (choose res!36 (Set Int) (forall ((a!6 Int)) (= (member a!6 set!0) (member (@ f!30 a!6) res!36)))))

(assert (not (or (not (= set!1 (insert (as emptyset Int) 1 2))) (= (map!6 (map!6 set!1 (lambda ((x!81 Int)) x!81)) (lambda ((x!82 Int)) x!82)) set!1))))

Mismatch between hasInstance and simplestValue

There are some mismatches between hasInstance and simplestValue

inox/src/main/scala/inox/ast/SymbolOps.scala

Line 906 in 7752948

def hasInstance(tpe: Type): Option[Boolean] = tpe match {

  • hasInstance returns true on types defined outside of Inox (such as ArrayType)
  • they don't seem to behave the same for ADTType, as hasInstance doesn't visit constructor fields?
  • they're different for TypeParameter, I guess that's expected?

Should we make them just one function (returning an Option), or is the distinction necessary?
And we should override these functions in Stainless for ArrayType? (always true?)

`--timeout` not respected

inox foo.smt2 --timeout=30 can happily run for dozens of minutes, where foo.smt2 is a TIP problem.

BitVector <-> Integer conversions

Since both Z3 [0] and CVC4 [1] apparently support interpreted conversions between bit vectors and integers (via bv2int, int2bv and bv2nat, nat2bv respectively), perhaps we could add support for such conversions in Inox, with a fallback for other solvers via recursive conversion procedures implemented as a theory encoder?

I have a PR for ScalaZ3 with a test for such Int<->BigInt conversions at epfl-lara/ScalaZ3#73.

[0] Z3Prover/z3#1481 (comment)
[1] cvc5/cvc5#750

/cc @samarion @jad-hamza @vkuncak

Issue with lambdas and untyped let bindings from Z3 4.8.5

On the tip file below, Z3 4.8.5 produces an output which contains this let binding:

(let ((a!1 (lambda ((x!1 T!83!10)) (or (= x!1 (T!83!11 1)) (= x!1 (T!83!11 6))))))
  (WithProof!4!1 a!1 0 true true)))

When Inox extracts lambdas, it needs to know whether it is extracting a Set, a Map, or a Bag. With this untyped, let binding, the information is missing. In the model produced by Z3 4.7.1, there is no let binding and variable a!1 is inlined in the body of the let. This gives enough context information for Inox to know which type to expect and how to extract the lambda.

One quick workaround is to inline let's before extracting, but not sure if this is ok? I'll try tomorrow and see how it goes.

(declare-datatypes () ((ProofOps!8 (ProofOps!9 (prop!31 Bool)))))

(declare-const thiss!36 ProofOps!8)

(declare-datatypes (T!37) ((LList!20 (LCons!18 (h!78 T!37) (t!89 (LList!20 T!37))) (LNil!18))))

(declare-const (par (T!83) (ls!12 (LList!20 (LList!20 T!83)))))

(declare-datatypes (A!10 B!6) ((WithProof!3 (WithProof!4 (x!145 A!10) (r!14 (=> A!10 B!6 Bool)) (proof!17 Bool) (prop!32 Bool)))))

(declare-const (par (T!83) (thiss!38 (WithProof!3 (Set T!83) (Set T!83)))))

(declare-datatypes (A!0) ((RelReasoning!7 (RelReasoning!8 (x!146 A!0) (prop!33 Bool)))))

(define-fun (par (A!95) (==$pipe!0 ((thiss!31 (RelReasoning!7 A!95)) (proof!2 Bool)) (WithProof!3 A!95 A!95) (WithProof!4 (x!146 thiss!31) (lambda ((x$1!0 A!95) (x$2!0 A!95)) (= x$1!0 x$2!0)) proof!2 (prop!33 thiss!31)))))

(define-fun (par (A!4) (any2RelReasoning!0 ((x!3 A!4)) (RelReasoning!7 A!4) (RelReasoning!8 x!3 true))))

(define-fun-rec (par (T!49) (content!7 ((thiss!3 (LList!20 T!49))) (Set T!49) (ite (is-LNil!18 thiss!3) (as emptyset T!49) (union (insert (as emptyset T!49) (h!78 thiss!3)) (content!7 (t!89 thiss!3)))))))

(define-fun-rec (par (T!48) (++!1 ((thiss!2 (LList!20 T!48)) (that!18 (LList!20 T!48))) (LList!20 T!48) (let ((res!33 (ite (is-LNil!18 thiss!2) that!18 (LCons!18 (h!78 thiss!2) (++!1 (t!89 thiss!2) that!18))))) (assume (and (= (content!7 res!33) (union (content!7 thiss!2) (content!7 that!18))) (or (not (= that!18 (as LNil!18 (LList!20 T!48)))) (= res!33 thiss!2))) res!33)))))

(define-fun-rec (par (T!44) (flatten!1 ((ls!6 (LList!20 (LList!20 T!44)))) (LList!20 T!44) (ite (is-LCons!18 ls!6) (++!1 (h!78 ls!6) (flatten!1 (t!89 ls!6))) (as LNil!18 (LList!20 T!44))))))

(define-fun (par (T!82) ($colon$colon!2 ((thiss!24 (LList!20 T!82)) (t!57 T!82)) (LList!20 T!82) (LCons!18 t!57 thiss!24))))

(define-fun trivial!0 () Bool true)

(declare-const (par (T!83) (that!25 (RelReasoning!7 (Set T!83)))))

(assert (par (T!83) (not (or (not (= thiss!36 (ProofOps!9 true))) (is-LNil!18 (as ls!12 (LList!20 (LList!20 T!83)))) (not (= (as thiss!38 (WithProof!3 (Set T!83) (Set T!83))) (==$pipe!0 (any2RelReasoning!0 (content!7 (flatten!1 ($colon$colon!2 (t!89 (as ls!12 (LList!20 (LList!20 T!83)))) (h!78 (as ls!12 (LList!20 (LList!20 T!83)))))))) trivial!0))) (not (= (as that!25 (RelReasoning!7 (Set T!83))) (any2RelReasoning!0 (as emptyset T!83)))) (and (prop!32 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83)))) (or (not (proof!17 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83))))) (@ (r!14 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83)))) (x!145 (as thiss!38 (WithProof!3 (Set T!83) (Set T!83)))) (x!146 (as that!25 (RelReasoning!7 (Set T!83)))))))))))

(check-sat)

wrong answer on a problem

On the following TIP problem, inox foo.smt2 answers SAT (both using nativez3 and smt-cvc4 as solvers), but the problem is unsatisfiable.

; UNSAT

; find a sorted list of length 3, that is a palindrome, and has sum 1
; this is impossible because the 1 should be in the middle (palindrome),
; but then the list is not sorted anymore

(declare-datatypes () ((nat (s (select_s_0 nat)) 
                            (z))))
(define-funs-rec
   ((plus ((x nat) (y nat)) nat))
   ((match x (case (s x2) (s (plus x2 y))) 
             (case z y))))
(define-funs-rec
   ((mult ((x_1 nat) (y_1 nat)) nat))
   ((match x_1 (case (s x2_1) (plus y_1 (mult x2_1 y_1))) 
               (case z z))))
(define-funs-rec
   ((leq ((x_2 nat) (y_2 nat)) Bool))
   ((match x_2
      (case (s x2_2) (match y_2 (case (s y2) (leq x2_2 y2)) 
                                (case z false))) 
      (case z true))))
(declare-datatypes
   ()
   ((list (cons (select_cons_0 nat) (select_cons_1 list)) 
          (nil))))
(define-funs-rec
   ((append ((x_3 list) (y_3 list)) list))
   ((match x_3 (case (cons n tail) (cons n (append tail y_3))) 
               (case nil y_3))))
(define-funs-rec
   ((rev ((l list)) list))
   ((match l
      (case (cons x_4 xs) (append (rev xs) (cons x_4 nil))) 
      (case nil nil))))
(define-funs-rec
   ((length ((l_1 list)) nat))
   ((match l_1 (case (cons x_5 tail_1) (s (length tail_1))) 
               (case nil z))))
(define-funs-rec
   ((sum ((l_2 list)) nat))
   ((match l_2 (case (cons x_6 tail_2) (plus x_6 (sum tail_2))) 
               (case nil z))))
(define-funs-rec
   ((sorted ((l_3 list)) Bool))
   ((match l_3
      (case (cons x_7 l2)
         (match l2
           (case (cons y_4 l3) (and (leq x_7 y_4) (sorted (cons y_4 l3)))) 
           (case nil true))) 
      (case nil true))))
(define-funs-rec ((num_3 () nat)) ((s (s (s z)))))
(assert-not
 (forall
    ((l_5 list))
    (not (and
          (and (and (sorted l_5) (= l_5 (rev l_5))) (= (sum l_5) (s z))) 
          (= (length l_5) num_3)))))
(check-sat)

Inox error when using set.toList in Stainless

Stainless program which calls set.toList inside a lambda errors out with Key not found error. Inside the example.zip is the example program and the tip and smt session outputs.

[  Info  ]   - Inferring measure for contains...
[  Info  ]  => Found measure for contains.
[  Info  ]   - Inferring measure for forall...
[  Info  ]  => Found measure for forall.
[  Info  ]   - Inferring measure for noDuplicates...
[  Info  ]  => Found measure for noDuplicates.
[  Info  ]  - Checking cache: 'precond. (call head[T]({   assert(thiss is MinimalEx...)' VC for randomCall1 @17:5...
[  Info  ] Cache miss: 'precond. (call head[T]({   assert(thiss is MinimalEx...)' VC for randomCall1 @17:5...
[  Info  ]  - Now solving 'precond. (call head[T]({   assert(thiss is MinimalEx...)' VC for randomCall1 @17:5...
[Internal] Error: key not found: x$135. Trace:
[Internal] - scala.collection.immutable.Map$EmptyMap$.apply(Map.scala:101)
[Internal] - scala.collection.immutable.Map$EmptyMap$.apply(Map.scala:99)
[Internal] - inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprStructure$12(TemplateGenerator.scala:143)
[Internal] - scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[Internal] - scala.collection.immutable.Set$Set1.foreach(Set.scala:97)
[Internal] - scala.collection.TraversableLike.map(TraversableLike.scala:238)
[Internal] - scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[Internal] - scala.collection.AbstractSet.scala$collection$SetLike$$super$map(Set.scala:51)
[Internal] - scala.collection.SetLike.map(SetLike.scala:104)
[Internal] - scala.collection.SetLike.map$(SetLike.scala:104)
[Internal] - scala.collection.AbstractSet.map(Set.scala:51)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprStructure(TemplateGenerator.scala:143)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprStructure$(TemplateGenerator.scala:78)
[Internal] - inox.solvers.unrolling.UnrollingSolver$templates$.mkExprStructure(UnrollingSolver.scala:854)
[Internal] - inox.solvers.unrolling.LambdaTemplates$LambdaTemplate$.apply(LambdaTemplates.scala:63)
[Internal] - inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:384)
[Internal] - inox.solvers.unrolling.TemplateGenerator.$anonfun$mkExprClauses$9(TemplateGenerator.scala:434)
[Internal] - scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - scala.collection.TraversableLike.map(TraversableLike.scala:238)
[Internal] - scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[Internal] - scala.collection.immutable.List.map(List.scala:298)
[Internal] - inox.solvers.unrolling.TemplateGenerator.rec$1(TemplateGenerator.scala:434)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprClauses(TemplateGenerator.scala:437)
[Internal] - inox.solvers.unrolling.TemplateGenerator.mkExprClauses$(TemplateGenerator.scala:237)
[Internal] - inox.solvers.unrolling.UnrollingSolver$templates$.mkExprClauses(UnrollingSolver.scala:854)
[Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$.$anonfun$apply$1(FunctionTemplates.scala:49)
[Internal] - scala.collection.MapLike.getOrElse(MapLike.scala:131)
[Internal] - scala.collection.MapLike.getOrElse$(MapLike.scala:129)
[Internal] - scala.collection.AbstractMap.getOrElse(Map.scala:63)
[Internal] - inox.solvers.unrolling.FunctionTemplates$FunctionTemplate$.apply(FunctionTemplates.scala:36)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$38(FunctionTemplates.scala:240)
[Internal] - scala.Option.getOrElse(Option.scala:189)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$11(FunctionTemplates.scala:240)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.immutable.Set$Set1.foreach(Set.scala:97)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$8(FunctionTemplates.scala:163)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.$anonfun$unroll$8$adapted(FunctionTemplates.scala:161)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.IterableLike.foreach(IterableLike.scala:74)
[Internal] - scala.collection.IterableLike.foreach$(IterableLike.scala:73)
[Internal] - scala.collection.AbstractIterable.foreach(Iterable.scala:56)
[Internal] - inox.solvers.unrolling.FunctionTemplates$functionsManager$.unroll(FunctionTemplates.scala:161)
[Internal] - inox.solvers.unrolling.Templates.$anonfun$unroll$4(Templates.scala:82)
[Internal] - scala.collection.TraversableLike.$anonfun$flatMap$1(TraversableLike.scala:245)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - scala.collection.TraversableLike.flatMap(TraversableLike.scala:245)
[Internal] - scala.collection.TraversableLike.flatMap$(TraversableLike.scala:242)
[Internal] - scala.collection.immutable.List.flatMap(List.scala:355)
[Internal] - inox.solvers.unrolling.Templates.unroll(Templates.scala:82)
[Internal] - inox.solvers.unrolling.Templates.unroll$(Templates.scala:78)
[Internal] - inox.solvers.unrolling.UnrollingSolver$templates$.unroll(UnrollingSolver.scala:854)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$36(UnrollingSolver.scala:815)
[Internal] - scala.runtime.java8.JFunction1$mcVI$sp.apply(JFunction1$mcVI$sp.java:23)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.immutable.Range.foreach(Range.scala:158)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$33(UnrollingSolver.scala:814)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$2(UnrollingSolver.scala:810)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.$anonfun$checkAssumptions$1(UnrollingSolver.scala:554)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.checkAssumptions(UnrollingSolver.scala:836)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.checkAssumptions$(UnrollingSolver.scala:553)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:200)
[Internal] - inox.solvers.combinators.TimeoutSolver.checkAssumptions(TimeoutSolver.scala:47)
[Internal] - inox.solvers.combinators.TimeoutSolver.checkAssumptions$(TimeoutSolver.scala:39)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:200)
[Internal] - inox.tip.TipDebugger.checkAssumptions(TipDebugger.scala:101)
[Internal] - inox.tip.TipDebugger.checkAssumptions$(TipDebugger.scala:99)
[Internal] - inox.solvers.SolverFactory$$anon$6.checkAssumptions(SolverFactory.scala:200)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.check(UnrollingSolver.scala:88)
[Internal] - inox.solvers.unrolling.AbstractUnrollingSolver.check$(UnrollingSolver.scala:87)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:200)
[Internal] - inox.solvers.combinators.TimeoutSolver.check(TimeoutSolver.scala:35)
[Internal] - inox.solvers.combinators.TimeoutSolver.check$(TimeoutSolver.scala:28)
[Internal] - inox.solvers.SolverFactory$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:200)
[Internal] - inox.tip.TipDebugger.check(TipDebugger.scala:96)
[Internal] - inox.tip.TipDebugger.check$(TipDebugger.scala:94)
[Internal] - inox.solvers.SolverFactory$$anon$6.check(SolverFactory.scala:200)
[Internal] - stainless.verification.VerificationChecker.$anonfun$checkVC$2(VerificationChecker.scala:233)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationChecker.checkVC(VerificationChecker.scala:228)
[Internal] - stainless.verification.VerificationChecker.checkVC$(VerificationChecker.scala:214)
[Internal] - stainless.verification.VerificationChecker$$anon$1.stainless$verification$VerificationCache$$super$checkVC(VerificationChecker.scala:345)
[Internal] - stainless.verification.VerificationCache.$anonfun$checkVC$1(VerificationCache.scala:87)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - stainless.verification.VerificationCache.checkVC(VerificationCache.scala:52)
[Internal] - stainless.verification.VerificationCache.checkVC$(VerificationCache.scala:42)
[Internal] - stainless.verification.VerificationChecker$$anon$1.checkVC(VerificationChecker.scala:345)
[Internal] - stainless.verification.VerificationChecker.$anonfun$checkVCs$2(VerificationChecker.scala:107)
[Internal] - scala.concurrent.Future$.$anonfun$traverse$1(Future.scala:850)
[Internal] - scala.collection.TraversableOnce.$anonfun$foldLeft$1(TraversableOnce.scala:160)
[Internal] - scala.collection.TraversableOnce.$anonfun$foldLeft$1$adapted(TraversableOnce.scala:160)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.IterableLike.foreach(IterableLike.scala:74)
[Internal] - scala.collection.IterableLike.foreach$(IterableLike.scala:73)
[Internal] - scala.collection.AbstractIterable.foreach(Iterable.scala:56)
[Internal] - scala.collection.TraversableOnce.foldLeft(TraversableOnce.scala:160)
[Internal] - scala.collection.TraversableOnce.foldLeft$(TraversableOnce.scala:158)
[Internal] - scala.collection.AbstractTraversable.foldLeft(Traversable.scala:108)
[Internal] - scala.concurrent.Future$.traverse(Future.scala:850)
[Internal] - stainless.verification.VerificationChecker.checkVCs(VerificationChecker.scala:97)
[Internal] - stainless.verification.VerificationChecker.checkVCs$(VerificationChecker.scala:90)
[Internal] - stainless.verification.VerificationChecker$Checker$1.checkVCs(VerificationChecker.scala:336)
[Internal] - stainless.verification.VerificationChecker.verify(VerificationChecker.scala:81)
[Internal] - stainless.verification.VerificationChecker.verify$(VerificationChecker.scala:77)
[Internal] - stainless.verification.VerificationChecker$Checker$1.verify(VerificationChecker.scala:336)
[Internal] - stainless.verification.VerificationChecker$.verify(VerificationChecker.scala:350)
[Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:111)
[Internal] - stainless.verification.VerificationRun.execute(VerificationComponent.scala:44)
[Internal] - stainless.ComponentRun.apply(Component.scala:105)
[Internal] - stainless.ComponentRun.apply$(Component.scala:97)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:44)
[Internal] - stainless.ComponentRun.apply(Component.scala:112)
[Internal] - stainless.ComponentRun.apply$(Component.scala:111)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:44)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processFunctionSymbols$3(SplitCallBack.scala:179)
[Internal] - scala.util.Try$.apply(Try.scala:213)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processFunctionSymbols$2(SplitCallBack.scala:179)
[Internal] - scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:238)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - scala.collection.TraversableLike.map(TraversableLike.scala:238)
[Internal] - scala.collection.TraversableLike.map$(TraversableLike.scala:231)
[Internal] - scala.collection.immutable.List.map(List.scala:298)
[Internal] - stainless.frontend.SplitCallBack.processFunctionSymbols(SplitCallBack.scala:178)
[Internal] - stainless.frontend.SplitCallBack.processFunction(SplitCallBack.scala:154)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3(SplitCallBack.scala:138)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3$adapted(SplitCallBack.scala:137)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:181)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:137)
[Internal] - stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:67)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:38)
[Internal] - java.base/java.lang.Thread.run(Thread.java:834)

Purity check

I'm opening this issue so that we remember that the isPure check in

inox/src/main/scala/inox/ast/SymbolOps.scala

Line 1332 in 082081b

if ((variablesOf(bd) contains vd.toVariable) || !isPure(e)(PurityOptions.Unchecked))

takes very long sometimes (some benchmarks that I will add take minutes
to run).

After doing some tests, it looks like the problem comes from the fact that
purity is checked by simplifying the whole formula. More precisely, the slowdown
seem to be coming from the simplification of Let's in simplify (https://github.com/epfl-lara/inox/blob/082081b77e80a0e95696c8649bdfb3d7f25a9d1d/src/main/scala/inox/transformers/SimplifierWithPC.scala lines 295-342).

String newline problem

The following code fails, even with the z3 solver.
Basically, I'm solving the equation var === "\n" but the result is strangely .n.n

import inox._
import inox.trees._
import inox.trees.dsl._
import inox.solvers._
import SolverResponses._

val prog = InoxProgram(
  Context.empty.copy(options = Options(Seq(Main.optDebug(Set(solvers.DebugSectionSolver)), optSelectedSolvers(Set("smt-cvc4"))))), Nil, List()
)
val solver = prog.getSolver.getNewSolver
val r = Variable(FreshIdentifier("r"), StringType, Set())
solver.assertCnstr(r === StringLiteral("\n"))
val rValue = solver.check(SolverResponses.Model) match {
  case SatWithModel(model) => model.vars(r.toVal  : inox.trees.ValDef) match {
    case StringLiteral(s) =>s
  }
}
assert(rValue == "\n", s"$rValue did not equal \\n")

Lookup failure in Definitions.scala (line 197), for apply.

Working with stainless to verify a heap sort. Let me know if you need to be able to reproduce this.

stainless  verified/src/main/scala/verified.scala --timeout=30 --debug=verification
[Warning ] Parallelism is disabled.
[Internal] Error: Lookup failed for function with symbol `apply$13`. Trace:
[Internal] - inox.ast.Definitions$AbstractSymbols.$anonfun$getFunction$1(Definitions.scala:197)
[Internal] - scala.Option.getOrElse(Option.scala:189)
[Internal] - inox.ast.Definitions$AbstractSymbols.getFunction(Definitions.scala:197)
[Internal] - inox.ast.Definitions$AbstractSymbols.getFunction$(Definitions.scala:196)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.getFunction(ClassSymbols.scala:18)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:53)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - inox.transformers.Traverser.traverse(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.traverse$(Traverser.scala:25)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$Traverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:21)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.transformers.GhostTraverser.$anonfun$traverse$5(GhostTraverser.scala:62)
[Internal] - stainless.transformers.GhostTraverser.$anonfun$traverse$5$adapted(GhostTraverser.scala:61)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:61)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:22)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2$adapted(GhostTraverser.scala:21)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:21)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:18)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.$anonfun$traverse$1(Traverser.scala:18)
[Internal] - stainless.transformers.Traverser.$anonfun$traverse$1$adapted(Traverser.scala:15)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:15)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:22)
[Internal] - stainless.extraction.methods.GhostTraverser.$anonfun$traverse$2$adapted(GhostTraverser.scala:21)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:21)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - inox.transformers.Traverser.traverse(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.traverse$(Traverser.scala:25)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$Traverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:21)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:51)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.$anonfun$traverse$4$adapted(Traverser.scala:29)
[Internal] - scala.collection.immutable.List.foreach(List.scala:392)
[Internal] - inox.transformers.Traverser.traverse(Traverser.scala:29)
[Internal] - inox.transformers.Traverser.traverse$(Traverser.scala:25)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$Traverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.Traverser.traverse(Traverser.scala:21)
[Internal] - stainless.transformers.Traverser.traverse$(Traverser.scala:12)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$transformers$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:71)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:52)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:32)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$oo$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse(GhostTraverser.scala:19)
[Internal] - stainless.extraction.oo.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$imperative$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse(GhostTraverser.scala:15)
[Internal] - stainless.extraction.imperative.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$methods$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse(GhostTraverser.scala:25)
[Internal] - stainless.extraction.methods.GhostTraverser.traverse$(GhostTraverser.scala:11)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:83)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:293)
[Internal] - stainless.transformers.GhostTraverser.traverse(GhostTraverser.scala:34)
[Internal] - stainless.transformers.GhostTraverser.traverse$(GhostTraverser.scala:28)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerfuns$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:28)
[Internal] - scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.withLocalFuns(GhostTraverser.scala:16)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse(GhostTraverser.scala:28)
[Internal] - stainless.extraction.innerfuns.GhostTraverser.traverse$(GhostTraverser.scala:21)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.stainless$extraction$innerclasses$GhostTraverser$$super$traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.$anonfun$traverse$2(GhostTraverser.scala:30)
[Internal] - scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.withLocalClasses(GhostTraverser.scala:18)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse(GhostTraverser.scala:30)
[Internal] - stainless.extraction.innerclasses.GhostTraverser.traverse$(GhostTraverser.scala:23)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality$ghostTraverser$.traverse(TreeSanitizer.scala:257)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality.$anonfun$sanitize$15(TreeSanitizer.scala:245)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality.$anonfun$sanitize$15$adapted(TreeSanitizer.scala:245)
[Internal] - scala.collection.immutable.Stream.foreach(Stream.scala:533)
[Internal] - stainless.extraction.xlang.TreeSanitizer$SoundEquality.sanitize(TreeSanitizer.scala:245)
[Internal] - stainless.extraction.xlang.TreeSanitizer.$anonfun$check$1(TreeSanitizer.scala:42)
[Internal] - scala.collection.immutable.List.flatMap(List.scala:338)
[Internal] - stainless.extraction.xlang.TreeSanitizer.check(TreeSanitizer.scala:42)
[Internal] - stainless.extraction.xlang.TreeSanitizer.check$(TreeSanitizer.scala:30)
[Internal] - stainless.extraction.xlang.TreeSanitizer$$anon$1.check(TreeSanitizer.scala:434)
[Internal] - stainless.extraction.xlang.TreeSanitizer.enforce(TreeSanitizer.scala:48)
[Internal] - stainless.extraction.xlang.TreeSanitizer.enforce$(TreeSanitizer.scala:45)
[Internal] - stainless.extraction.xlang.TreeSanitizer$$anon$1.enforce(TreeSanitizer.scala:434)
[Internal] - stainless.frontend.SplitCallBack.processFunctionSymbols(SplitCallBack.scala:160)
[Internal] - stainless.frontend.SplitCallBack.processFunction(SplitCallBack.scala:154)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3(SplitCallBack.scala:138)
[Internal] - stainless.frontend.SplitCallBack.$anonfun$processSymbols$3$adapted(SplitCallBack.scala:137)
[Internal] - scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[Internal] - scala.collection.Iterator.foreach(Iterator.scala:941)
[Internal] - scala.collection.Iterator.foreach$(Iterator.scala:941)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:181)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[Internal] - stainless.frontend.SplitCallBack.processSymbols(SplitCallBack.scala:137)
[Internal] - stainless.frontend.SplitCallBack.endExtractions(SplitCallBack.scala:67)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:38)
[Internal] - java.base/java.lang.Thread.run(Thread.java:834)
[Internal] Lookup failed for function with symbol `apply$13`
[Internal] Please inform the authors of Inox about this message
bash-3.2$

Integration of `rust-interop` in `master`

Landing the rust-interop features on master would have enormous benefits for the epfl-lara/rust-stainless project in terms of less maintenance for getting updates. This is under the condition that the features added/changed on the rust-interop branch can co-exist with the current master.

@samarion suggested the following changes to rust-interop before a potential merge:

  • I would add an option optFormat which can be either “tip” or “binary”
  • move deserializerMain into the Main object unless you need it in Stainless (and same for the optDeserialize option)
  • Then I’d create a parsing method in the Main with return type (Program, Option[Expr]) (or maybe Symbols instead of Program, depending on the API of the TIP parser’s parseScript method)
  • If the format option is “tip”, then call the current TIP parsing logic and return the resulting program and Some of the expression
  • If the format option is “binary”, deserialize the input and check if there’s a boolean method with some pre-defined name in the program, e.g. check. Then return the deserialized program (minus the check method) and the check method’s body as the expression. If no such method exists in the program, return None for the Option[Expr].
  • Then, if the returned option is Some, run solving on that expression.
  • In addition, I would add a boolean option optPrintProgram which, if true, has Inox print the program (and potential expression) returned by either the “tip” or “binary” parser.

StringSuite test fail with Z3 4.7.1 

$ sbt "it:testOnly *StringSuite* -- -z 28"
[info] Loading project definition from /path/inox/project
[info] Set current project to inox (in build file:/path/inox/)
[info] StringSuite:
[info] -  28: Non-ASCII string encoding solvr=smt-z3 *** FAILED *** (472 milliseconds)
[info]   scala.MatchError: WrappedArray(-17, -65, -125) (of class scala.collection.mutable.WrappedArray$ofByte)
[info]   at inox.solvers.theories.ASCIIStringEncoder$class.inox$solvers$theories$ASCIIStringEncoder$$decodeFirstByte(ASCIIStringEncoder.scala:35)
[info]   at inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:68)
[info]   at inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:84)
[info]   at inox.solvers.theories.ASCIIStringEncoder$decoder$.unescape$1(ASCIIStringEncoder.scala:84)
[info]   at inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:87)
[info]   at inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:291)
[info]   at inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:310)
[info]   at inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27)
[info]   at inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:63)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.decode(SolverFactory.scala:198)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$class.decodeOrSimplest$1(UnrollingSolver.scala:455)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:461)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$39.apply(UnrollingSolver.scala:461)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:184)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:184)
[info]   at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[info]   at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[info]   at scala.collection.immutable.Map$Map1.foreach(Map.scala:116)
[info]   at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[info]   at scala.collection.AbstractTraversable.map(Traversable.scala:104)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:184)
[info]   at inox.solvers.unrolling.UnrollingSolver$ModelWrapper.getModel(UnrollingSolver.scala:783)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$class.inox$solvers$unrolling$AbstractUnrollingSolver$$extractTotalModel(UnrollingSolver.scala:461)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:597)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$checkAssumptions$1.apply(UnrollingSolver.scala:472)
[info]   at scala.util.Try$.apply(Try.scala:192)
[info]   at inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[info]   at inox.utils.TimerStorage.run(Timer.scala:88)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:472)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:198)
[info]   at inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:198)
[info]   at inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:61)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.checkAssumptions(SolverFactory.scala:198)
[info]   at inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:86)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:198)
[info]   at inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.inox$tip$TipDebugger$$super$check(SolverFactory.scala:198)
[info]   at inox.tip.TipDebugger$class.check(TipDebugger.scala:56)
[info]   at inox.solvers.SolverFactory$$anonfun$getFromName$4$$anon$8.check(SolverFactory.scala:198)
[info]   at inox.solvers.SimpleSolverAPI$class.solveSAT(SimpleSolverAPI.scala:35)
[info]   at inox.solvers.SimpleSolverAPI$$anon$1.solveSAT(SimpleSolverAPI.scala:57)
[info]   at inox.solvers.unrolling.StringSuite$$anonfun$6.apply(StringSuite.scala:57)
[info]   at inox.solvers.unrolling.StringSuite$$anonfun$6.apply(StringSuite.scala:54)
[info]   at inox.TestSuite$$anonfun$test$2$$anonfun$apply$2.apply$mcV$sp(TestSuite.scala:57)
[info]   at inox.TestSuite$$anonfun$test$2$$anonfun$apply$2.apply(TestSuite.scala:57)
[info]   at inox.TestSuite$$anonfun$test$2$$anonfun$apply$2.apply(TestSuite.scala:57)
[info]   at org.scalatest.OutcomeOf$class.outcomeOf(OutcomeOf.scala:85)
[info]   at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
[info]   at org.scalatest.Transformer.apply(Transformer.scala:22)
[info]   at org.scalatest.Transformer.apply(Transformer.scala:20)
[info]   at org.scalatest.FunSuiteLike$$anon$1.apply(FunSuiteLike.scala:186)
[info]   at org.scalatest.TestSuite$class.withFixture(TestSuite.scala:196)
[info]   at org.scalatest.FunSuite.withFixture(FunSuite.scala:1560)
[info]   at org.scalatest.FunSuiteLike$class.invokeWithFixture$1(FunSuiteLike.scala:183)
[info]   at org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:196)
[info]   at org.scalatest.FunSuiteLike$$anonfun$runTest$1.apply(FunSuiteLike.scala:196)
[info]   at org.scalatest.SuperEngine.runTestImpl(Engine.scala:289)
[info]   at org.scalatest.FunSuiteLike$class.runTest(FunSuiteLike.scala:196)
[info]   at org.scalatest.FunSuite.runTest(FunSuite.scala:1560)
[info]   at org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:229)
[info]   at org.scalatest.FunSuiteLike$$anonfun$runTests$1.apply(FunSuiteLike.scala:229)
[info]   at org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:396)
[info]   at org.scalatest.SuperEngine$$anonfun$traverseSubNodes$1$1.apply(Engine.scala:384)
[info]   at scala.collection.immutable.List.foreach(List.scala:381)
[info]   at org.scalatest.SuperEngine.traverseSubNodes$1(Engine.scala:384)
[info]   at org.scalatest.SuperEngine.org$scalatest$SuperEngine$$runTestsInBranch(Engine.scala:379)
[info]   at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:461)
[info]   at org.scalatest.FunSuiteLike$class.runTests(FunSuiteLike.scala:229)
[info]   at org.scalatest.FunSuite.runTests(FunSuite.scala:1560)
[info]   at org.scalatest.Suite$class.run(Suite.scala:1147)
[info]   at org.scalatest.FunSuite.org$scalatest$FunSuiteLike$$super$run(FunSuite.scala:1560)
[info]   at org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:233)
[info]   at org.scalatest.FunSuiteLike$$anonfun$run$1.apply(FunSuiteLike.scala:233)
[info]   at org.scalatest.SuperEngine.runImpl(Engine.scala:521)
[info]   at org.scalatest.FunSuiteLike$class.run(FunSuiteLike.scala:233)
[info]   at org.scalatest.FunSuite.run(FunSuite.scala:1560)
[info]   at org.scalatest.tools.Framework.org$scalatest$tools$Framework$$runSuite(Framework.scala:314)
[info]   at org.scalatest.tools.Framework$ScalaTestTask.execute(Framework.scala:480)
[info]   at sbt.TestRunner.runTest$1(TestFramework.scala:76)
[info]   at sbt.TestRunner.run(TestFramework.scala:85)
[info]   at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
[info]   at sbt.TestFramework$$anon$2$$anonfun$$init$$1$$anonfun$apply$8.apply(TestFramework.scala:202)
[info]   at sbt.TestFramework$.sbt$TestFramework$$withContextLoader(TestFramework.scala:185)
[info]   at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
[info]   at sbt.TestFramework$$anon$2$$anonfun$$init$$1.apply(TestFramework.scala:202)
[info]   at sbt.TestFunction.apply(TestFramework.scala:207)
[info]   at sbt.Tests$.sbt$Tests$$processRunnable$1(Tests.scala:239)
[info]   at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
[info]   at sbt.Tests$$anonfun$makeSerial$1.apply(Tests.scala:245)
[info]   at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
[info]   at sbt.std.Transform$$anon$3$$anonfun$apply$2.apply(System.scala:44)
[info]   at sbt.std.Transform$$anon$4.work(System.scala:63)
[info]   at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
[info]   at sbt.Execute$$anonfun$submit$1$$anonfun$apply$1.apply(Execute.scala:228)
[info]   at sbt.ErrorHandling$.wideConvert(ErrorHandling.scala:17)
[info]   at sbt.Execute.work(Execute.scala:237)
[info]   at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
[info]   at sbt.Execute$$anonfun$submit$1.apply(Execute.scala:228)
[info]   at sbt.ConcurrentRestrictions$$anon$4$$anonfun$1.apply(ConcurrentRestrictions.scala:159)
[info]   at sbt.CompletionService$$anon$2.call(CompletionService.scala:28)
[info]   at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[info]   at java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:511)
[info]   at java.util.concurrent.FutureTask.run(FutureTask.java:266)
[info]   at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
[info]   at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
[info]   at java.lang.Thread.run(Thread.java:748)
[info] Run completed in 1 second, 38 milliseconds.
[info] Total number of tests run: 1
[info] Suites: completed 1, aborted 0
[info] Tests: succeeded 0, failed 1, canceled 0, ignored 0, pending 0
[info] *** 1 TEST FAILED ***
[error] Failed tests:
[error]         inox.solvers.unrolling.StringSuite
[error] (it:testOnly) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 3 s, completed 13 sept. 2018 13:41:11

Model for abstract functions

I might have missed something in inox --help, but is there an option to print the model when the solver states "SAT"?

Two tip files representing the same Stainless VC have a large running time difference

Inox consistently finishes in 1 or 2 seconds for inox fast.tip (the VC is false and Inox finds a counter-example), but may timeout 5 minutes for inox slow.tip, or sometimes finish in ~20 sec. For context, fast.tip was generated by a standard command-line call of Stainless, while slow.tip was generated by going through the ComponentTestSuite.

Some notable differences: fast.tip doesn't refer to Mapping, and the ContractInterface datatype declaration is much shorter in fast.tip

fast.tip

(declare-datatypes () ((State!3 (Default!2) (Default1!2) (Default2!2) (Default3!2) (Finished!2) (WaitingForData!2) (WaitingForLender!2) (WaitingForPayback!2))))

(declare-datatypes (T!12) ((List!3 (Cons!2 (h!47 T!12) (t!57 (List!3 T!12))) (Nil!2))))

(declare-datatypes () ((Address!2 (Address!3 (id!4 Int)))))

(declare-datatypes () ((ContractInterface!1 (ERC20Token!2 (s!19 Int)) (LoanContract!2 (borrower!2 Address!2) (wantedAmount!2 (_ BitVec 256)) (premiumAmount!2 (_ BitVec 256)) (tokenAmount!2 (_ BitVec 256)) (tokenName!2 String) (tokenContractAddress!2 ContractInterface!1) (daysToLend!2 (_ BitVec 256)) (currentState!2 State!3) (start!3 (_ BitVec 256)) (lender!2 Address!2) (visitedStates!2 (List!3 State!3))) (Open!2 (x!99 Int)) (Open!3 (x!100 Int)))))

(declare-const thiss!28 ContractInterface!1)

(define-fun (par (T!42) (isEmpty!1 ((thiss!29 (List!3 T!42))) Bool (ite (is-Nil!2 thiss!29) true false))))

(define-fun-rec (par (T!40) (isPrefix!0 ((l1!12 (List!3 T!40)) (l2!10 (List!3 T!40))) Bool (ite (is-Nil!2 l1!12) true (ite (and (is-Cons!2 l1!12) (is-Cons!2 l2!10) (= (h!47 l1!12) (h!47 l2!10))) (isPrefix!0 (t!57 l1!12) (t!57 l2!10)) false)))))

(define-fun-rec (par (T!44) (size!1 ((thiss!31 (List!3 T!44))) Int (let ((x$1!4 (ite (is-Nil!2 thiss!31) 0 (+ 1 (size!1 (t!57 thiss!31)))))) (assume (>= x$1!4 0) x$1!4)))))

(define-fun-rec (par (T!45) (content!4 ((thiss!32 (List!3 T!45))) (Set T!45) (ite (is-Nil!2 thiss!32) (as emptyset T!45) (union (insert (as emptyset T!45) (h!47 thiss!32)) (content!4 (t!57 thiss!32)))))))

(define-fun-rec (par (T!46) (|:+!0| ((thiss!33 (List!3 T!46)) (t!7 T!46)) (List!3 T!46) (let ((res!8 (ite (is-Nil!2 thiss!33) (Cons!2 t!7 thiss!33) (Cons!2 (h!47 thiss!33) (|:+!0| (t!57 thiss!33) t!7))))) (assume (assume (is-Cons!2 res!8) (and (= (size!1 res!8) (+ (size!1 thiss!33) 1)) (= (content!4 res!8) (union (content!4 thiss!33) (insert (as emptyset T!46) t!7))))) res!8)))))

(define-fun-rec (par (T!43) (reverse!0 ((thiss!30 (List!3 T!43))) (List!3 T!43) (let ((res!9 (ite (is-Nil!2 thiss!30) thiss!30 (|:+!0| (reverse!0 (t!57 thiss!30)) (h!47 thiss!30))))) (assume (and (= (size!1 res!9) (size!1 thiss!30)) (= (content!4 res!9) (content!4 thiss!30))) res!9)))))

(define-fun expected!0 () (List!3 State!3) (Cons!2 (let ((v!70 WaitingForData!2)) (assume (is-WaitingForData!2 v!70) v!70)) (Cons!2 (let ((v!71 WaitingForLender!2)) (assume (is-WaitingForLender!2 v!71) v!71)) (as Nil!2 (List!3 State!3)))))

(datatype-invariant thiss!16 ContractInterface!1 (=> (is-LoanContract!2 thiss!16) (is-ERC20Token!2 (tokenContractAddress!2 thiss!16))))

(assert (not (=> (and (is-LoanContract!2 thiss!28) (not (isEmpty!1 (visitedStates!2 thiss!28)))) (not (isPrefix!0 (reverse!0 (visitedStates!2 thiss!28)) expected!0)))))

(check-sat)

; check-assumptions required here, but not part of tip standard

slow.tip

(declare-datatypes () ((Address!3 (Address!4 (id!10 Int)))))

(declare-datatypes (A!47 B!33) ((Mapping!5 (Mapping!6 (underlying!12 (=> A!47 B!33))))))

(declare-datatypes (T!10) ((List!8 (Cons!5 (h!94 T!10) (t!111 (List!8 T!10))) (Nil!5))))

(declare-datatypes () ((State!5 (Default!2) (Default1!2) (Default2!2) (Default3!2) (Finished!2) (WaitingForData!2) (WaitingForLender!2) (WaitingForPayback!2))))

(declare-datatypes () ((ContractInterface!2 (BasicContract1!3 (other!6 Address!3)) (BasicInterface1!3) (CallWithEther1!3 (other!7 ContractInterface!2)) (DuplicateIdentifier1!3 (i!35 (_ BitVec 256))) (DuplicateIdentifier2!3 (i!36 (_ BitVec 256))) (DynRequire1!3) (ERC20Token!2 (s!24 Int)) (EtherTransfer1!3 (other!8 Address!3)) (LoanContract!2 (borrower!2 Address!3) (wantedAmount!2 (_ BitVec 256)) (premiumAmount!2 (_ BitVec 256)) (tokenAmount!2 (_ BitVec 256)) (tokenName!2 String) (tokenContractAddress!2 ContractInterface!2) (daysToLend!2 (_ BitVec 256)) (currentState!2 State!5) (start!4 (_ BitVec 256)) (lender!2 Address!3) (visitedStates!2 (List!8 State!5))) (MappingType1!3 (m!4 (Mapping!5 Address!3 (_ BitVec 256)))) (MappingType2!3 (m!5 (Mapping!5 Address!3 (Mapping!5 Address!3 (_ BitVec 256))))) (Open!3 (x!179 Int)) (Open!4 (x!180 Int)) (Open!5 (x!181 Int)) (PositiveUint!3) (VotingToken!3 (rewardToken!2 ContractInterface!2) (opened!2 Bool) (closed!2 Bool) (votingAddresses!2 (List!8 Address!3)) (numberOrAlternatives!2 (_ BitVec 256)) (owner!2 Address!3) (name!2 String) (symbol!2 String) (decimals!2 (_ BitVec 8)) (totalSupply!5 (_ BitVec 256)) (balances!8 (Mapping!5 Address!3 (_ BitVec 256))) (allowed!2 (Mapping!5 Address!3 (Mapping!5 Address!3 (_ BitVec 256)))) (participants!7 (List!8 Address!3))))))

(declare-const thiss!5 ContractInterface!2)

(define-fun (par (T!82) (isEmpty!1 ((thiss!31 (List!8 T!82))) Bool (ite (is-Nil!5 thiss!31) true false))))

(define-fun-rec (par (T!38) (isPrefix!0 ((l1!12 (List!8 T!38)) (l2!10 (List!8 T!38))) Bool (ite (is-Nil!5 l1!12) true (ite (and (is-Cons!5 l1!12) (is-Cons!5 l2!10) (= (h!94 l1!12) (h!94 l2!10))) (isPrefix!0 (t!111 l1!12) (t!111 l2!10)) false)))))

(define-fun-rec (par (T!85) (size!0 ((thiss!34 (List!8 T!85))) Int (let ((x$1!4 (ite (is-Nil!5 thiss!34) 0 (+ 1 (size!0 (t!111 thiss!34)))))) (assume (>= x$1!4 0) x$1!4)))))

(define-fun-rec (par (T!83) (content!4 ((thiss!32 (List!8 T!83))) (Set T!83) (ite (is-Nil!5 thiss!32) (as emptyset T!83) (union (insert (as emptyset T!83) (h!94 thiss!32)) (content!4 (t!111 thiss!32)))))))

(define-fun-rec (par (T!84) (|:+!0| ((thiss!33 (List!8 T!84)) (t!7 T!84)) (List!8 T!84) (let ((res!5 (ite (is-Nil!5 thiss!33) (Cons!5 t!7 thiss!33) (Cons!5 (h!94 thiss!33) (|:+!0| (t!111 thiss!33) t!7))))) (assume (assume (is-Cons!5 res!5) (and (= (size!0 res!5) (+ (size!0 thiss!33) 1)) (= (content!4 res!5) (union (content!4 thiss!33) (insert (as emptyset T!84) t!7))))) res!5)))))

(define-fun-rec (par (T!86) (reverse!0 ((thiss!35 (List!8 T!86))) (List!8 T!86) (let ((res!6 (ite (is-Nil!5 thiss!35) thiss!35 (|:+!0| (reverse!0 (t!111 thiss!35)) (h!94 thiss!35))))) (assume (and (= (size!0 res!6) (size!0 thiss!35)) (= (content!4 res!6) (content!4 thiss!35))) res!6)))))

(define-fun expected!0 () (List!8 State!5) (Cons!5 (let ((v!101 WaitingForData!2)) (assume (is-WaitingForData!2 v!101) v!101)) (Cons!5 (let ((v!102 WaitingForLender!2)) (assume (is-WaitingForLender!2 v!102) v!102)) (as Nil!5 (List!8 State!5)))))

(datatype-invariant thiss!41 ContractInterface!2 (and (=> (is-CallWithEther1!3 thiss!41) (is-CallWithEther1!3 (other!7 thiss!41))) (=> (is-LoanContract!2 thiss!41) (is-ERC20Token!2 (tokenContractAddress!2 thiss!41))) (=> (is-VotingToken!3 thiss!41) (is-Open!5 (rewardToken!2 thiss!41)))))

(assert (not (=> (and (is-LoanContract!2 thiss!5) (not (isEmpty!1 (visitedStates!2 thiss!5)))) (not (isPrefix!0 (reverse!0 (visitedStates!2 thiss!5)) expected!0)))))

(check-sat)

Choose under lamba

In this PR epfl-lara/stainless#946, I changed the way VCs are generated in the type-checker, and the following file is now valid:
https://github.com/epfl-lara/stainless/blob/965b0ec485e62715003738e73605bd4dbb5da1da/frontends/benchmarks/verification/invalid/Equations1.scala
But I was expecting the second equations to fail, because the makeEqual(x, y) evidence shouldn't "leak".

I've narrowed the issue to this tip file, on which Inox returns UNSAT (I've tried z3 and cvc4 1.8).
Surprisingly, removing the assertion on eq2 makes Inox return SAT. (removing the assertion on eq1 makes Inox return SAT as well)

(declare-datatypes (A B) ((RAEquations (RaCons (lhs (=> A)) (rhs (=> A)) (ev (=> B))))))
(datatype-invariant (par (A B) this (RAEquations A B) (= (@ (lhs this)) (@ (rhs this)))))

(declare-datatypes () ((Unit (Uu))))

(define-fun makeEqual ((x Int) (y Int)) Unit (choose unused Unit (= x y)))

(declare-const x Int)
(declare-const y Int)

(declare-const eq1 (RAEquations Int Unit))
(declare-const eq2 (RAEquations Int Unit))

(assert (= eq1 (RaCons (lambda () x) (lambda () x) (lambda () (makeEqual x y)))))
(assert (= eq2 (RaCons (lambda () x) (lambda () x) (lambda () Uu))))
(assert (not (= y x)))

(check-sat)

Z3Optimizer not present in Windows compilation of Inox

I wanted to compile inox on windows by using sbt publish-local. However, I get the following problem:

[info] Compiling 122 Scala sources to C:\...\inox\target\scala-2.11\classes...
[info] Wrote C:\...\inox\target\scala-2.11\inox_2.11-1.0.2-55-g499e6bc.pom
[info] Main Scala API documentation to C:\...\inox\target\scala-2.11\api...
[info] :: delivering :: ch.epfl.lara#inox_2.11;1.0.2-55-g499e6bc :: 1.0.2-55-g499e6bc :: integration :: Thu Apr 06 19:40:27 CEST 2017
[info]  delivering ivy file to C:\...\inox\target\scala-2.11\ivy-1.0.2-55-g499e6bc.xml
[error] C:\...\inox\src\main\scala\inox\solvers\z3\NativeZ3Optimizer.scala:8: object Z3Optimizer is not a member of package z3.scala
[error] import z3.scala.{Z3Optimizer => ScalaZ3Optimizer, _}
[error]        ^

I looked into the provided JAR file, but the Z3Optimizer class is indeed not present in the windows version of unmanaged/scalaz3-win-64-2.11.jar, whereas it appears correctly in the unix version of the same file.

What should I do to update this file?

Inox reports an error for invalid (unlucky) models found with `--feeling-lucky`

This is an issue eg. in epfl-lara/stainless#274 (comment).

With --feeling-lucky and --check-models on, this test fails because Inox reports an invalid (unlucky) model:

> stainless-scalac/run --vc-cache=false --check-models --feeling-lucky ../benchmarks/verification/valid/IgnoredField.scala
[info] Running stainless.Main --vc-cache=false --check-models --feeling-lucky ../benchmarks/verification/valid/IgnoredField.scala
[info] [Warning ] Parallelism is disabled.
[info] [  Info  ]  - Now solving 'body assertion' VC for test @43:5...
[info] [  Info  ]  - Result for 'body assertion' VC for test @43:5:
[info] [  Info  ]  => VALID
[info] [  Info  ]  - Now solving 'body assertion' VC for test @44:5...
[info] [ Error  ] Something went wrong. The model should have been valid, yet we got this:
[info] [ Error  ]   res: TrieMapWrapper[BigInt, BigInt] -> TrieMapWrapper[BigInt, BigInt](0)
[info] [ Error  ]
[info] [ Error  ]   contains[BigInt,BigInt](thiss: TrieMapWrapper[K, V], k: K) -> if (thiss == TrieMapWrapper[BigInt, BigInt](0) && k == 1) {
[info] [ Error  ]     false
[info] [ Error  ]   } else {
[info] [ Error  ]     choose((res$226: Boolean) => true)
[info] [ Error  ]   }
[info] [ Error  ] for formula ∀k: BigInt. ¬contains[BigInt, BigInt](res, k)
[info] [  Info  ]  - Result for 'body assertion' VC for test @44:5:
[info] [  Info  ]  => VALID
[info] [  Info  ]   ┌───────────────────┐
[info] [  Info  ] ╔═╡ stainless summary ╞══════════════════════════════════════════════════════════════════════════════════╗
[info] [  Info  ] ║ └───────────────────┘                                                                                  ║
[info] [  Info  ] ║ test  body assertion  valid  nativez3  ../benchmarks/verification/valid/IgnoredField.scala:43:5  0.179 ║
[info] [  Info  ] ║ test  body assertion  valid  nativez3  ../benchmarks/verification/valid/IgnoredField.scala:44:5  0.218 ║
[info] [  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[info] [  Info  ] ║ total: 2    valid: 2    (0 from cache) invalid: 0    unknown: 0    time:   0.397                       ║
[info] [  Info  ] ╚════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[info] [  Info  ] Shutting down executor service.
[success] Total time: 6 s, completed Aug 15, 2018 1:09:36 PM

I have tried without success so far to prevent Inox from reporting invalid lucky models, perhaps you could give it a look yourself? A simple test for that is to run stainless in my ignore-field branch with stainless-scalac/run --vc-cache=false --check-models --feeling-lucky ../benchmarks/verification/valid/IgnoredField.scala, and check that no invalid model is reported.

Check behaviour of model with choose

This warning should be fixed and tests added to ensure the feature is acting as expected.

[warn] inox/src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala:880: comparing values of types (inox.ast.Identifier, Seq[ModelWrapper.this.model.program.trees.Type]) and inox.ast.Identifier using `==' will always yield false
[warn]     def getChoose(id: Identifier): Option[t.Expr] = model.chooses.find(_._1 == id).map(_._2)

See here.

Error due to Z3?

I'm using Z3 4.5.1 and getting many errors when running sbt test it:test. Is it perhaps because of some change in Z3? (It doesn't seem to be because of #31)

For example:

[info] - 295: flatMap is associative solvr=smt-z3-opt lucky=false check=false assum=true model=0 *** FAILED *** (85 milliseconds)
[info]   inox.package$FatalError: Unexpected error from z3 solver: line 284 column 22: unsat assumptions construction is not enabled, use command (set-option :produce-unsat-assumptions true)

Error with default parameters in require

The following program:

package object exError {
  def foo(x: Boolean=true): Boolean = x

  def bar(): Unit = {
    require(foo())

    ()
  }
}

Yields the following error:

[ Error  ] bar$0 depends on missing dependencies: foo$default$1$0.
[Internal] Missing some nodes in Registry: foo$default$1$0
[Internal] Please inform the authors of Inox about this message

Error with GADTs and function types

When executing stainless on the following program:

package object exError {

  sealed abstract class T[A]
  case class C_T[A](x: E[A => Boolean]) extends T[A]

  sealed abstract class E[A]
  case class C_E[A](x: A) extends E[A => Boolean]
}

I get the following error message:

[Internal] Error: Type error: x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]   val x$95: Object = x$96
[Internal]   @unchecked x.value(x$95) is Boolean
[Internal] })), expected Boolean, 
[Internal] found <untyped>
[Internal] 
[Internal] Typing explanation:
[Internal] x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]   val x$95: Object = x$96
[Internal]   @unchecked x.value(x$95) is Boolean
[Internal] })) is of type <untyped>
[Internal]   x is C_T is of type Boolean
[Internal]     x is of type T[A]
[Internal]   isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]     val x$95: Object = x$96
[Internal]     @unchecked x.value(x$95) is Boolean
[Internal]   })) is of type <untyped>
[Internal]     x.x is of type <untyped>
[Internal]       x is of type T[A]
[Internal]     (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]       val x$95: Object = x$96
[Internal]       @unchecked x.value(x$95) is Boolean
[Internal]     }) is of type <untyped>
[Internal]       x is Function1 && ∀x$96: A. (true ==> {
[Internal]         val x$95: Object = x$96
[Internal]         @unchecked x.value(x$95) is Boolean
[Internal]       }) is of type <untyped>
[Internal]         x is Function1 is of type <untyped>
[Internal]           x is of type Object
[Internal]         ∀x$96: A. (true ==> {
[Internal]           val x$95: Object = x$96
[Internal]           @unchecked x.value(x$95) is Boolean
[Internal]         }) is of type <untyped>
[Internal]           true ==> {
[Internal]             val x$95: Object = x$96
[Internal]             @unchecked x.value(x$95) is Boolean
[Internal]           } is of type <untyped>
[Internal]             true is of type Boolean
[Internal]             val x$95: Object = x$96
[Internal]             @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal]               x$96 is of type A
[Internal]               @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal]                 @unchecked x.value(x$95) is of type <untyped>
[Internal]                   @unchecked x.value is of type <untyped>
[Internal]                     x.value is of type <untyped>
[Internal]                       x is of type Object
[Internal]                   x$95 is of type Object because isE was instantiated with  with type (Object,(Object) => Boolean) => Boolean. Trace:
[Internal] - inox.ast.TypeOps$TypeErrorException$.apply(TypeOps.scala:22)
[Internal] - inox.ast.TypeOps$class.typeCheck(TypeOps.scala:89)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.typeCheck(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormedFunction(Definitions.scala:215)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormedFunction(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormedSymbols$2.apply(Definitions.scala:210)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$ensureWellFormedSymbols$2.apply(Definitions.scala:210)
[Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
[Internal] - scala.collection.immutable.HashMap$HashMap1.foreach(HashMap.scala:221)
[Internal] - scala.collection.immutable.HashMap$HashTrieMap.foreach(HashMap.scala:428)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormedSymbols(Definitions.scala:210)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.stainless$extraction$oo$Definitions$AbstractSymbols$$super$ensureWellFormedSymbols(ClassSymbols.scala:13)
[Internal] - stainless.extraction.oo.Definitions$AbstractSymbols$class.ensureWellFormedSymbols(Definitions.scala:135)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormedSymbols(ClassSymbols.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply$mcV$sp(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3$$anonfun$apply$1.apply(Definitions.scala:207)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3.apply(Definitions.scala:207)
[Internal] - inox.ast.Definitions$AbstractSymbols$$anonfun$3.apply(Definitions.scala:207)
[Internal] - inox.utils.Lazy.get(Lazy.scala:13)
[Internal] - inox.ast.Definitions$AbstractSymbols$class.ensureWellFormed(Definitions.scala:206)
[Internal] - stainless.extraction.oo.ClassSymbols$ClassSymbols.ensureWellFormed(ClassSymbols.scala:13)
[Internal] - stainless.extraction.oo.TypeEncoding$class.extractSymbols(TypeEncoding.scala:1168)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extractSymbols(TypeEncoding.scala:1242)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extractSymbols(TypeEncoding.scala:1242)
[Internal] - stainless.extraction.CachingPhase$class.extract(ExtractionPipeline.scala:91)
[Internal] - stainless.extraction.oo.TypeEncoding$$anon$1.extract(TypeEncoding.scala:1242)
[Internal] - stainless.extraction.utils.DebugPipeline$$anonfun$5.apply(DebugPipeline.scala:67)
[Internal] - stainless.extraction.utils.DebugPipeline$$anonfun$5.apply(DebugPipeline.scala:67)
[Internal] - scala.util.Try$.apply(Try.scala:192)
[Internal] - inox.utils.TimerStorage.runAndGetTime(Timer.scala:93)
[Internal] - inox.utils.TimerStorage.run(Timer.scala:88)
[Internal] - stainless.extraction.utils.DebugPipeline$class.extract(DebugPipeline.scala:67)
[Internal] - stainless.extraction.utils.DebugPipeline$$anon$1.extract(DebugPipeline.scala:98)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.extraction.ExtractionPipeline$$anon$1.extract(ExtractionPipeline.scala:28)
[Internal] - stainless.ComponentRun$class.extract(Component.scala:75)
[Internal] - stainless.verification.VerificationRun.extract(VerificationComponent.scala:37)
[Internal] - stainless.ComponentRun$class.apply(Component.scala:86)
[Internal] - stainless.verification.VerificationRun.apply(VerificationComponent.scala:37)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16$$anonfun$6.apply(StainlessCallBack.scala:247)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16$$anonfun$6.apply(StainlessCallBack.scala:247)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
[Internal] - scala.collection.immutable.List.map(List.scala:285)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16.apply(StainlessCallBack.scala:247)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1$$anonfun$apply$16.apply(StainlessCallBack.scala:222)
[Internal] - scala.collection.TraversableLike$WithFilter$$anonfun$foreach$1.apply(TraversableLike.scala:733)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:174)
[Internal] - scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:732)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1.apply(StainlessCallBack.scala:222)
[Internal] - stainless.frontend.StainlessCallBack$$anonfun$processSymbols$1.apply(StainlessCallBack.scala:222)
[Internal] - scala.collection.immutable.List.foreach(List.scala:381)
[Internal] - stainless.frontend.StainlessCallBack.processSymbols(StainlessCallBack.scala:222)
[Internal] - stainless.frontend.StainlessCallBack.apply(StainlessCallBack.scala:59)
[Internal] - stainless.frontends.scalac.StainlessExtraction$Phase.apply(StainlessExtraction.scala:34)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$applyPhase$1.apply$mcV$sp(Global.scala:440)
[Internal] - scala.tools.nsc.Global$GlobalPhase.withCurrentUnit(Global.scala:431)
[Internal] - scala.tools.nsc.Global$GlobalPhase.applyPhase(Global.scala:440)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$run$1.apply(Global.scala:398)
[Internal] - scala.tools.nsc.Global$GlobalPhase$$anonfun$run$1.apply(Global.scala:398)
[Internal] - scala.collection.Iterator$class.foreach(Iterator.scala:893)
[Internal] - scala.collection.AbstractIterator.foreach(Iterator.scala:1336)
[Internal] - scala.tools.nsc.Global$GlobalPhase.run(Global.scala:398)
[Internal] - scala.tools.nsc.Global$Run.compileUnitsInternal(Global.scala:1501)
[Internal] - scala.tools.nsc.Global$Run.compileUnits(Global.scala:1486)
[Internal] - scala.tools.nsc.Global$Run.compileSources(Global.scala:1481)
[Internal] - scala.tools.nsc.Global$Run.compile(Global.scala:1582)
[Internal] - stainless.frontends.scalac.ScalaCompiler$Factory$$anon$1.onRun(ScalaCompiler.scala:127)
[Internal] - stainless.frontend.ThreadedFrontend$$anon$1.run(ThreadedFrontend.scala:31)
[Internal] - java.lang.Thread.run(Thread.java:748)
[Internal] Type error: x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]   val x$95: Object = x$96
[Internal]   @unchecked x.value(x$95) is Boolean
[Internal] })), expected Boolean, 
[Internal] found <untyped>
[Internal] 
[Internal] Typing explanation:
[Internal] x is C_T && isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]   val x$95: Object = x$96
[Internal]   @unchecked x.value(x$95) is Boolean
[Internal] })) is of type <untyped>
[Internal]   x is C_T is of type Boolean
[Internal]     x is of type T[A]
[Internal]   isE(x.x, (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]     val x$95: Object = x$96
[Internal]     @unchecked x.value(x$95) is Boolean
[Internal]   })) is of type <untyped>
[Internal]     x.x is of type <untyped>
[Internal]       x is of type T[A]
[Internal]     (x: Object) => x is Function1 && ∀x$96: A. (true ==> {
[Internal]       val x$95: Object = x$96
[Internal]       @unchecked x.value(x$95) is Boolean
[Internal]     }) is of type <untyped>
[Internal]       x is Function1 && ∀x$96: A. (true ==> {
[Internal]         val x$95: Object = x$96
[Internal]         @unchecked x.value(x$95) is Boolean
[Internal]       }) is of type <untyped>
[Internal]         x is Function1 is of type <untyped>
[Internal]           x is of type Object
[Internal]         ∀x$96: A. (true ==> {
[Internal]           val x$95: Object = x$96
[Internal]           @unchecked x.value(x$95) is Boolean
[Internal]         }) is of type <untyped>
[Internal]           true ==> {
[Internal]             val x$95: Object = x$96
[Internal]             @unchecked x.value(x$95) is Boolean
[Internal]           } is of type <untyped>
[Internal]             true is of type Boolean
[Internal]             val x$95: Object = x$96
[Internal]             @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal]               x$96 is of type A
[Internal]               @unchecked x.value(x$95) is Boolean is of type <untyped>
[Internal]                 @unchecked x.value(x$95) is of type <untyped>
[Internal]                   @unchecked x.value is of type <untyped>
[Internal]                     x.value is of type <untyped>
[Internal]                       x is of type Object
[Internal]                   x$95 is of type Object because isE was instantiated with  with type (Object,(Object) => Boolean) => Boolean
[Internal] Please inform the authors of Inox about this message

Error in documentation when compiling

When I run sbt clean compile I get the following error, simillar to #97 :

[info] Running (fork) tut.TutMain /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md /home/stevan/Documents/master_project/inox/doc .*\.(md|markdown|txt|htm|html) -deprecation -unchecked -feature
[info] [tut] compiling: /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md
[error] WARNING: An illegal reflective access operation has occurred
[error] WARNING: Illegal reflective access by z3.Z3Wrapper (file:/home/stevan/Documents/master_project/inox/unmanaged/scalaz3-unix-64-2.12.jar) to field java.lang.ClassLoader.sys_paths
[error] WARNING: Please consider reporting this to the maintainers of z3.Z3Wrapper
[error] WARNING: Use --illegal-access=warn to enable warnings of further illegal reflective access operations
[error] WARNING: All illegal access operations will be denied in a future release
[error] null
[error] java.lang.NullPointerException
[error]         at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2646)
[error]         at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:830)
[error]         at java.base/java.lang.System.loadLibrary(System.java:1870)
[error]         at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:110)
[error]         at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:49)
[error]         at inox.solvers.SolverFactory$.liftedTree1$1(SolverFactory.scala:29)
[error]         at inox.solvers.SolverFactory$.hasNativeZ3$lzycompute(SolverFactory.scala:28)
[error]         at inox.solvers.SolverFactory$.hasNativeZ3(SolverFactory.scala:28)
[error]         at inox.solvers.SolverFactory$.$anonfun$fallbacks$1(SolverFactory.scala:78)
[error]         at inox.solvers.SolverFactory$.getFromName(SolverFactory.scala:100)
[error]         at inox.solvers.SolverFactory$.apply(SolverFactory.scala:356)
[error]         at inox.solvers.SolverFactory$.apply(SolverFactory.scala:364)
[error]         at inox.package$$anon$1$$anon$2.createSolver(package.scala:76)
[error]         at inox.Semantics.$anonfun$getSolver$1(Semantics.scala:31)
[error]         at inox.utils.Cache.cached(Caches.scala:14)
[error]         at inox.utils.Cache.cached$(Caches.scala:11)
[error]         at inox.utils.LruCache.cached(Caches.scala:20)
[error]         at inox.Semantics.getSolver(Semantics.scala:31)
[error]         at inox.Semantics.getSolver$(Semantics.scala:28)
[error]         at inox.package$$anon$1$$anon$2.getSolver(package.scala:65)
[error]         at inox.Program.getSolver(Program.scala:60)
[error]         at inox.Program.getSolver$(Program.scala:57)
[error]         at inox.Program$$anon$1.getSolver(Program.scala:93)
[error]         at $line22.$read$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$.<init>(<console>:27)
[error]         at $line22.$read$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$$iw$.<clinit>(<console>)
[error]         at $line22.$eval$.$print$lzycompute(<console>:7)
[error]         at $line22.$eval$.$print(<console>:6)
[error]         at $line22.$eval.$print(<console>)
[error]         at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[error]         at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
[error]         at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[error]         at java.base/java.lang.reflect.Method.invoke(Method.java:566)
[error]         at scala.tools.nsc.interpreter.IMain$ReadEvalPrint.call(IMain.scala:742)
[error]         at scala.tools.nsc.interpreter.IMain$Request.loadAndRun(IMain.scala:1018)
[error]         at scala.tools.nsc.interpreter.IMain.$anonfun$interpret$1(IMain.scala:574)
[error]         at scala.reflect.internal.util.ScalaClassLoader.asContext(ScalaClassLoader.scala:41)
[error]         at scala.reflect.internal.util.ScalaClassLoader.asContext$(ScalaClassLoader.scala:37)
[error]         at scala.reflect.internal.util.AbstractFileClassLoader.asContext(AbstractFileClassLoader.scala:41)
[error]         at scala.tools.nsc.interpreter.IMain.loadAndRunReq$1(IMain.scala:573)
[error]         at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:600)
[error]         at scala.tools.nsc.interpreter.IMain.interpret(IMain.scala:570)
[error]         at tut.Tut$.$anonfun$interp$6(Tut.scala:56)
[error]         at tut.felix.IO$Primitive.unsafePerformIO(IO.scala:76)
[error]         at tut.felix.IO$Compute.loop$1(IO.scala:117)
[error]         at tut.felix.IO$Compute.unsafePerformIO(IO.scala:125)
[error]         at tut.felix.Syntax$IOOps.$anonfun$withOut$2(Syntax.scala:34)
[error]         at scala.util.DynamicVariable.withValue(DynamicVariable.scala:62)
[error]         at scala.Console$.withOut(Console.scala:167)
[error]         at tut.felix.Syntax$IOOps.$anonfun$withOut$1(Syntax.scala:34)
[error]         at tut.felix.IO$Primitive.unsafePerformIO(IO.scala:76)
[error]         at tut.felix.IO$Compute.loop$1(IO.scala:121)
[error]         at tut.felix.IO$Compute.unsafePerformIO(IO.scala:125)
[error]         at tut.TutMain$.main(TutMain.scala:8)
[error]         at tut.TutMain.main(TutMain.scala)
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:203
[error] java.lang.NullPointerException
[error]   at java.base/java.lang.ClassLoader.loadLibrary(ClassLoader.java:2646)
[error]   at java.base/java.lang.Runtime.loadLibrary0(Runtime.java:830)
[error]   at java.base/java.lang.System.loadLibrary(System.java:1870)
[error]   at com.microsoft.z3.Native.<clinit>(Native.java:13)
[error]   at z3.Z3Wrapper.z3VersionString(Z3Wrapper.java:75)
[error]   at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:51)
[error]   at inox.solvers.SolverFactory$.liftedTree1$1(SolverFactory.scala:29)
[error]   at inox.solvers.SolverFactory$.hasNativeZ3$lzycompute(SolverFactory.scala:28)
[error]   at inox.solvers.SolverFactory$.hasNativeZ3(SolverFactory.scala:28)
[error]   at inox.solvers.SolverFactory$.$anonfun$fallbacks$1(SolverFactory.scala:78)
[error]   at inox.solvers.SolverFactory$.getFromName(SolverFactory.scala:100)
[error]   at inox.solvers.SolverFactory$.apply(SolverFactory.scala:356)
[error]   at inox.solvers.SolverFactory$.apply(SolverFactory.scala:364)
[error]   at inox.package$$anon$1$$anon$2.createSolver(package.scala:76)
[error]   at inox.Semantics.$anonfun$getSolver$1(Semantics.scala:31)
[error]   at inox.utils.Cache.cached(Caches.scala:14)
[error]   at inox.utils.Cache.cached$(Caches.scala:11)
[error]   at inox.utils.LruCache.cached(Caches.scala:20)
[error]   at inox.Semantics.getSolver(Semantics.scala:31)
[error]   at inox.Semantics.getSolver$(Semantics.scala:28)
[error]   at inox.package$$anon$1$$anon$2.getSolver(package.scala:65)
[error]   at inox.Program.getSolver(Program.scala:60)
[error]   at inox.Program.getSolver$(Program.scala:57)
[error]   at inox.Program$$anon$1.getSolver(Program.scala:93)
[error]   ... 31 elided
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:204
[error] <console>:28: error: not found: value solver
[error]        solver.assertCnstr(Not(prop))
[error]        ^
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:205
[error] <console>:27: error: not found: value solver
[error]        solver.check(SolverResponses.Simple) // Should return `Unsat`
[error]        ^
[error] [tut] *** Error reported at /home/stevan/Documents/master_project/inox/src/main/doc/tutorial.md:206
[error] <console>:27: error: not found: value solver
[error]        solver.free()
[error]        ^
[error] Exception in thread "main" tut.TutException: Tut execution failed.
[error]         at tut.TutMain$.$anonfun$runl$6(TutMain.scala:17)
[error]         at tut.felix.IO$Compute.loop$1(IO.scala:121)
[error]         at tut.felix.IO$Compute.unsafePerformIO(IO.scala:125)
[error]         at tut.TutMain$.main(TutMain.scala:8)
[error]         at tut.TutMain.main(TutMain.scala)
[error] java.lang.RuntimeException: Nonzero exit code returned from runner: 1
[error]         at scala.sys.package$.error(package.scala:26)
[error]         at tut.TutPlugin$.$anonfun$tutOne$1(TutPlugin.scala:149)
[error]         at scala.util.Success.foreach(Try.scala:249)
[error]         at tut.TutPlugin$.tutOne(TutPlugin.scala:149)
[error]         at tut.TutPlugin$.$anonfun$tutAll$1(TutPlugin.scala:157)
[error]         at scala.collection.immutable.List.flatMap(List.scala:334)
[error]         at tut.TutPlugin$.tutAll(TutPlugin.scala:157)
[error]         at tut.TutPlugin$.handleUpdate$1(TutPlugin.scala:106)
[error]         at tut.TutPlugin$.$anonfun$projectSettings$29(TutPlugin.scala:111)
[error]         at sbt.util.FileFunction$.$anonfun$cached$4(FileFunction.scala:147)
[error]         at sbt.util.Difference.apply(Tracked.scala:313)
[error]         at sbt.util.Difference.apply(Tracked.scala:293)
[error]         at sbt.util.FileFunction$.$anonfun$cached$3(FileFunction.scala:143)
[error]         at sbt.util.Difference.apply(Tracked.scala:313)
[error]         at sbt.util.Difference.apply(Tracked.scala:288)
[error]         at sbt.util.FileFunction$.$anonfun$cached$2(FileFunction.scala:142)
[error]         at tut.TutPlugin$.$anonfun$projectSettings$25(TutPlugin.scala:111)
[error]         at scala.Function1.$anonfun$compose$1(Function1.scala:44)
[error]         at sbt.internal.util.$tilde$greater.$anonfun$$u2219$1(TypeFunctions.scala:40)
[error]         at sbt.std.Transform$$anon$4.work(System.scala:67)
[error]         at sbt.Execute.$anonfun$submit$2(Execute.scala:269)
[error]         at sbt.internal.util.ErrorHandling$.wideConvert(ErrorHandling.scala:16)
[error]         at sbt.Execute.work(Execute.scala:278)
[error]         at sbt.Execute.$anonfun$submit$1(Execute.scala:269)
[error]         at sbt.ConcurrentRestrictions$$anon$4.$anonfun$submitValid$1(ConcurrentRestrictions.scala:178)
[error]         at sbt.CompletionService$$anon$2.call(CompletionService.scala:37)
[error]         at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[error]         at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
[error]         at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
[error]         at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
[error]         at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
[error]         at java.base/java.lang.Thread.run(Thread.java:834)
[error] (tutQuick) Nonzero exit code returned from runner: 1
[error] Total time: 82 s, completed May 4, 2020, 5:56:43 PM

Retrieving defunctionalized string?

Is it possible to retrieve the encoded string for an Inox program before it gets sent off to a solver?
I.e.: the script where higher order functions, dependent types, etc have been removed (or at least rewritten to be FO compatible)

I know if I set debug flags a certain way it will write the .smt2 files to an 'smt-sessions' folder-- though as far as I know this only gets written once the solver is invoked. Is there some native way to programmatically get a string (or at least a File) corresponding to a converted program?

(Apologies if this is in the wrong place; wasn't sure whether to post this on StackOverflow or here)

Unsat file reported as SAT 

(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
(declare-datatypes () ((T (TT (body S)))))
(define-fun t () T (TT (C 22 5)))
(assert (not (let ((g f)) (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ g r2))) g) 22) 5))))
(check-sat)
(define-fun f () (=> Int Int) (lambda ((loc Int)) 0))
(declare-datatypes () ((S (N) (C (r Int) (e Int)))))
(declare-datatypes () ((T (TT (body S)))))
(define-fun t () T (TT (C 22 5)))
(assert (not (= (@ (ite (is-C (body t)) (lambda ((r2 Int)) (ite (= r2 (r (body t))) (e (body t)) (@ f r2))) f) 22) 5)))
(check-sat)

The first file is reported as SAT (--check-models invalidates the model) while the second one (where the let g has been removed) is correctly reported as UNSAT.

The SMT file generated by Inox is:

; Options: -in -smt2
(set-option :produce-unsat-assumptions true)
(declare-fun start!1 () Bool)
(assert start!1)
(declare-fun bs!1 () Bool)
(declare-fun b!8 () Bool)
(assert (= bs!1 (and b!8 start!1)))
(declare-fun lambda!5 () Int)
(declare-fun lambda!4 () Int)
(assert (=> bs!1 (not (= lambda!5 lambda!4))))
(assert (=> b!8 true))
(declare-fun order!1 () Int)
(declare-fun dynLambda!0 (Int Int) Int)
(assert (=> b!8 (< (dynLambda!0 order!1 lambda!4) (dynLambda!0 order!1 lambda!5))))
(declare-fun c!4 () Bool)
(assert (=> start!1 (= c!4 true)))
(declare-fun e!5 () Int)
(declare-fun dynLambda!1 (Int Int) Int)
(assert (=> start!1 (not (= (dynLambda!1 e!5 22) 5))))
(assert (=> b!8 (= e!5 lambda!5)))
(declare-fun b!9 () Bool)
(assert (=> b!9 (= e!5 lambda!4)))
(assert (= (and start!1 c!4) b!8))
(assert (= (and start!1 (not c!4)) b!9))
(declare-fun b_lambda!1 () Bool)
(assert (=> (not b_lambda!1) (not start!1)))
(declare-fun m!1 () Bool)
(assert (=> start!1 m!1))
(check-sat (not b_lambda!1))
(check-sat)
(get-model)
(declare-fun b_lambda!3 () Bool)
(assert (= b_lambda!1 (or start!1 b_lambda!3)))
(declare-fun bs!2 () Bool)
(declare-fun d!1 () Bool)
(assert (= bs!2 (and d!1 start!1)))
(assert (=> bs!2 (= (dynLambda!1 lambda!4 22) 0)))
(assert (=> start!1 d!1))
(check-sat (not b_lambda!3))
(get-model)

The variable b_lambda!3 from the end only appears in the assertion (= b_lambda!1 (or start!1 b_lambda!3)), and is unconstrained because start!1 must be true.

Can this be due to #105 (which touched let's)?

wrong answer

This problem should be "unsat" (unless I wrote it wrong?), but inox reports "sat"

version: 5a8f96e
backends z3 and cvc4 both trigger the error.

; UNSAT

; the classic "pigeonhole" principle: trying to fit 5 pigeons
; into 4 holes is bound to fail.

(declare-sort hole 0)
(declare-fun h1 () hole)
(declare-fun h2 () hole)
(declare-fun h3 () hole)
(declare-fun h4 () hole)
(declare-fun p1 () hole)
(declare-fun p2 () hole)
(declare-fun p3 () hole)
(declare-fun p4 () hole)
(declare-fun p5 () hole)
(assert
 (and
  (not (= h1 h2))
  (not (= h1 h3))
  (not (= h1 h4))
  (not (= h2 h3))
  (not (= h2 h4))
  (not (= h3 h4))
 ))
(assert
  (and
    (not (= p1 p2))
    (not (= p1 p3))
    (not (= p1 p4))
    (not (= p1 p5))
    (not (= p2 p3))
    (not (= p2 p4))
    (not (= p2 p5))
    (not (= p3 p4))
    (not (= p3 p5))
    (not (= p4 p5))
  ))
; map pigeons to holes
(assert
 (forall ((p hole)) (or (= p h1) (= p h2) (= p h3) (= p h4))))
(check-sat)

String conversion problem

To reproduce this problem, use the following self-contained script in a console having inox:

import inox._
import inox.trees._
import inox.trees.dsl._
import inox.solvers._

val prog = InoxProgram(
  Context.empty.copy(options = Options(Seq(Main.optDebug(Set(solvers.DebugSectionSolver)), optSelectedSolvers(Set("smt-cvc4"))))), Nil, List()
)
val solver = prog.getSolver.getNewSolver
implicit class StringVars(sc: StringContext) {
  def l() = StringLiteral(sc.parts.mkString(""))
}
implicit class Cct(s: Expr) {
  def +&(other: Expr) = StringConcat(s, other)
}
val f4 = Variable(FreshIdentifier("f4"), FunctionType(Seq(StringType), StringType), Set())
val cstr = f4 === \("x"::StringType)(x => x +& l" ?")
solver.assertCnstr(cstr)
solver.check(SolverResponses.Model)

Although the formula is trivial, the result is unexpected:

java.lang.ClassCastException: inox.ast.Types$StringType$ cannot be cast to inox.ast.Types$ADTType
  at inox.ast.TreeDeconstructor$$anonfun$deconstruct$50.apply(Extractors.scala:126)
  at inox.ast.TreeDeconstructor$$anonfun$deconstruct$50.apply(Extractors.scala:126)
  at inox.ast.TreeTransformer$class.transform(TreeOps.scala:145)
  at inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:102)
  at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:133)
  at inox.ast.TreeTransformer$$anonfun$3.apply(TreeOps.scala:132)
  at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
  at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
  at scala.collection.immutable.List.foreach(List.scala:381)
  at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
  at scala.collection.immutable.List.map(List.scala:285)
  at inox.ast.TreeTransformer$class.transform(TreeOps.scala:132)
  at inox.solvers.theories.ASCIIStringEncoder$decoder$.transform(ASCIIStringEncoder.scala:102)
  at inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:238)
  at inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:257)
  at inox.ast.TreeTransformer$TreeTransformerComposition$class.transform(TreeOps.scala:238)
  at inox.ast.TreeTransformer$$anon$1.transform(TreeOps.scala:257)
  at inox.ast.ProgramTransformer$class.decode(ProgramOps.scala:27)
  at inox.ast.ProgramTransformer$$anon$4.decode(ProgramOps.scala:46)
  at inox.solvers.unrolling.AbstractUnrollingSolver$class.decode(UnrollingSolver.scala:64)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.decode(SolverFactory.scala:248)
  at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:540)
  at inox.solvers.unrolling.AbstractUnrollingSolver$$anonfun$43.apply(UnrollingSolver.scala:540)
  at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:178)
  at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$$anonfun$6.apply(UnrollingSolver.scala:178)
  at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
  at scala.collection.TraversableLike$$anonfun$map$1.apply(TraversableLike.scala:234)
  at scala.collection.immutable.Map$Map3.foreach(Map.scala:161)
  at scala.collection.TraversableLike$class.map(TraversableLike.scala:234)
  at scala.collection.AbstractTraversable.map(Traversable.scala:104)
  at inox.solvers.unrolling.AbstractUnrollingSolver$ModelWrapper$class.getModel(UnrollingSolver.scala:178)
  at inox.solvers.unrolling.UnrollingSolver$ModelWrapper.getModel(UnrollingSolver.scala:848)
  at inox.solvers.unrolling.AbstractUnrollingSolver$class.extractTotalModel(UnrollingSolver.scala:540)
  at inox.solvers.unrolling.AbstractUnrollingSolver$class.checkAssumptions(UnrollingSolver.scala:667)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$checkAssumptions(SolverFactory.scala:248)
  at inox.solvers.combinators.TimeoutSolver$class.checkAssumptions(TimeoutSolver.scala:47)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$tip$TipDebugger$$super$checkAssumptions(SolverFactory.scala:248)
  at inox.tip.TipDebugger$class.checkAssumptions(TipDebugger.scala:62)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.checkAssumptions(SolverFactory.scala:248)
  at inox.solvers.unrolling.AbstractUnrollingSolver$class.check(UnrollingSolver.scala:87)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$solvers$combinators$TimeoutSolver$$super$check(SolverFactory.scala:248)
  at inox.solvers.combinators.TimeoutSolver$class.check(TimeoutSolver.scala:35)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.inox$tip$TipDebugger$$super$check(SolverFactory.scala:248)
  at inox.tip.TipDebugger$class.check(TipDebugger.scala:57)
  at inox.solvers.SolverFactory$$anonfun$getFromName$6$$anon$6.check(SolverFactory.scala:248)

The error is the same if I use z3 instead of CVC4.

Parse error with CVC4 1.8 

$ cvc4 --version
This is CVC4 version 1.8-prerelease [git master 7988675c]

With CVC4 above, every benchmark I have thrown to Inox has yielded:

Internal solver error in cvc4: Solver encountered exception: smtlib.parser.Parser$UnexpectedTokenException: Unexpected token at position: (9, 1). Expected: [OParen]. Found: unsat

I am unable to build latest CVC4 master at the moment, so I only tested with commit 7988675c .

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.