search

viperproject / silicon

Symbolic-execution-based verifier for the Viper intermediate verification language.
Mozilla Public License 2.0
81 stars 34 forks source link

Incorrect evaluation of OR #47

Closed viper-admin closed 4 years ago

viper-admin commented 11 years ago

Created by @mschwerhoff on 2013-09-22 22:28 Last updated on 2013-09-22 22:41

This example verifies, although it shouldn't:

method test01(x: Int, y: Int, z: Int)
  requires (z == x || z == y)
{
  assert z == y
}

I briefly looked at the smtlib2 output and the error seems to be related to the short-circuiting evaluation of OR.

viper-admin commented 11 years ago

@mschwerhoff commented on 2013-09-22 22:41

Fixed https://github.com/viperproject/silicon/issues/47 of Silicon. The problem was, that the auxiliary path conditions resulting from the short-circuiting evaluation of 'e0 || e1' still contained '!e0', which was temporarily in the state while evaluating 'e1'.

→ <<cset https://github.com/viperproject/silicon/commit/ba7382f77f9c2f8475e240f1134b729d871de3c4>>

viper-admin commented 11 years ago

@mschwerhoff on 2013-09-22 22:41:

  • changed state from new to resolved