-
Notifications
You must be signed in to change notification settings - Fork 30
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
Smtlib2 #721
Smtlib2 #721
Conversation
48d880d
to
9a23ab0
Compare
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/AssumeSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/DataRaceSolver.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/ModelChecker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Outdated
Show resolved
Hide resolved
dartagnan/src/main/java/com/dat3m/dartagnan/encoding/ProverWithTracker.java
Show resolved
Hide resolved
I have no clue why the diff from the browser shows changes related to PRs recently merged to I don't get those locally. Attached if the diff I get locally wrt |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
This PR creates a wrapper around the
ProverEnvironment
which allows to dump the encoding to an smtlib2 file.Attached are the encodings of ticketlock both with eager and lazy methods, and this is the output of z3
output.zip