adding error detection for nested predicates

[jyoo980]

Tested with

field left: Int
field right: Int
field middle: Int
field elem: Int
field next: Ref

predicate list(this: Ref) 
{
  acc(this.elem) && acc(this.next) &&
        (this.next != null ==> list(this.next))
}

predicate deep(this: Ref)
{
  acc(this.middle, write) && list(this)
}

predicate mid(this: Ref) {
  acc(this.middle, write) && deep(this)
}

predicate triple(this: Ref) {
  acc(this.left) && acc(this.right) && acc(this.right) && 
  acc(this.left) && acc(this.right) && acc(this.right) &&
  acc(this.left) && acc(this.right) && acc(this.right) &&
  acc(this.left) && acc(this.right) && mid(this)
}

result

jyoo@lambda silicon % ./silicon.sh --z3Exe '/Users/jyoo/dev/oss/z3/build/z3'  ~/Desktop/viper-tests/nested.vpr
Silicon 1.1-SNAPSHOT (f52b14f8+)
Predicate: `list` is recursive. Will not be inlined
Predicate: `mid` is a nested predicate. Will not be inlined
Predicate: `deep` is a nested predicate. Will not be inlined
Predicate: `list` is a nested predicate. Will not be inlined
successfully returned
Silicon finished verification successfully in 3.68s.

should resolve #20

[jyoo980]

We really do live in a (software) society

Bottom text

[jyoo980]

Closing this in favour of #23