Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ITE expressions are not always eliminated #25

Open
wies opened this issue May 16, 2018 · 0 comments
Open

ITE expressions are not always eliminated #25

wies opened this issue May 16, 2018 · 0 comments
Labels

Comments

@wies
Copy link
Owner

wies commented May 16, 2018

Example:

procedure foo(x: Int, f: Map<Int, Map<Int, Int>>)
  requires forall i: Int, j: Int :: f[i][j] == (i < j ? 1 : 0)
  ensures false
{}

Error: unexpected expression at File "/home/siddharth/grasshopper/test.spl", line 2, columns 48-61
Raised at file "pervasives.ml", line 32, characters 17-33
Called from file "src/frontends/spl/splTranslator.ml", line 405, characters 21-43
Called from file "src/frontends/spl/splTranslator.ml", line 393, characters 17-45
Called from file "src/frontends/spl/splTranslator.ml", line 527, characters 16-43
Called from file "src/frontends/spl/splTranslator.ml", line 534, characters 14-40
Called from file "src/frontends/spl/splTranslator.ml", line 662, characters 12-67
Called from file "src/frontends/spl/splTranslator.ml", line 793, characters 24-83
Called from file "map.ml", line 315, characters 19-42
Called from file "src/frontends/spl/splTranslator.ml", line 791, characters 4-868
Called from file "src/frontends/spl/splTranslator.ml" (inlined), line 834, characters 2-13
Called from file "src/main/grasshopper.ml", line 119, characters 13-46
Called from file "src/main/grasshopper.ml", line 215, characters 18-62
@wies wies added the bug label Nov 5, 2018
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant