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

smtlib parsing: assertion hit when parsing wrongly typed equation #26

Closed
quicquid opened this issue Feb 21, 2020 · 1 comment
Closed

Comments

@quicquid
Copy link
Contributor

quicquid commented Feb 21, 2020

Please consider the following smtlib script:

(set-logic AUFLIA)
(declare-fun notindomain (Int) Int)
(assert (forall ((i Int))
                (= (notindomain i) (or (< i 0) (< 5 i)) )))
(check-sat)

It contains a type error because notindomain should be of type Int to Bool. When I run dolmen on the file, I receive the following error message:

Error While typing: (= (notindomain (i)) (or (< (i) 0) (< 5 (i))))
File '/tmp/test.smt2', line 6, character 16-57:
The term: (Fatal error: exception File "src/standard/expr.ml", line 484, characters 6-12: Assertion failed

The error occurs in pretty printing (the assertion requires an infix operator to have at least 2 arguments) so it might hide the actual error.

@Gbury Gbury mentioned this issue Feb 28, 2020
@Gbury
Copy link
Owner

Gbury commented Apr 29, 2020

This was solved by PR#27 but apparently github didn't automatically close the issue, ^^

@Gbury Gbury closed this as completed Apr 29, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants