Java Modeling Language (JML) / Feature Requests / #151 Prover has no support for XOR in invariants

#151 Prover has no support for XOR in invariants

Milestone: OpenJML

Status: open

Owner: David Cok

Labels: OpenJML (4)

Module: OpenJML

Priority: 1

Updated: 2013-10-27

Created: 2011-03-10

Creator: Anonymous

Private: No

warning: Prover failed: BallotJournal(Candidate): Binary operator not implemented for Yices: 60:(assert+ (= assert$138$138$UndefinedNullReference$68 (=> true (/= this$ NULL))))

Binary operator not implemented for Yices, and it would be nice if it was

Discussion

Comment has been marked as spam.
Undo

View and moderate all "feature-requests Discussion" comments posted by this user

Mark all as spam, and block user from posting to "Feature Requests"
Anonymous - 2011-03-10

priority: 5 --> 1

- **priority**: 5 --> 1

Add attachments
Cancel
You seem to have CSS turned off. Please don't fill out this field.

You seem to have CSS turned off. Please don't fill out this field.

New Attachment:
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

David Cok - 2012-12-02

milestone: --> OpenJML
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Joseph Kiniry - 2012-12-02

Recall that xor is negated bi-implication. Sometimes this makes for an easier mapping if you happen to have n-ary <->.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

David Cok - 2013-10-27

Group: --> OpenJML
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

David Cok - 2013-10-27

Module: --> OpenJML
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Prover has no support for XOR in invariants

Searches

Help

#151 Prover has no support for XOR in invariants

Discussion