[Symex] Only generate counterexample when the user asks for it#67
[Symex] Only generate counterexample when the user asks for it#67dawa6183 wants to merge 2 commits intouuverifiers:masterfrom
Conversation
zafer-esen
left a comment
zafer-esen
left a comment
There was a problem hiding this comment.
Thanks for this PR @dawa6183 ! I left a few comments for improvement.
In addition, I think an improvement to this PR (or possibly another PR) would be to add verification for solutions and counterexamples -- it doesn't look like we are doing this right now. You can do something similar to what happens in the CEGAR engine, you can search for HornWrapper.verifyCEX in HornWrapper.scala.
| else constraint | ||
|
|
||
| if (constraint.negatedConjs.isEmpty) { | ||
| if (constraint.negatedConjs.isEmpty || |
There was a problem hiding this comment.
This change is not mentioned in the PR description. If this is another issue I think it would be great to have it as a separate PR.
| var printInfo = false | ||
|
|
||
| // This might be set to true in SymexHornWrapper | ||
| var generateCounterExample = false |
There was a problem hiding this comment.
We could maybe use GlobalParameters.needFullCEX (can access with GlobalParameters.get.needFullCEX) instead of introducing a new local parameter for the same?
There was a problem hiding this comment.
needFullCEX is not true when simplifiedCEX is true but I can remove generateCounterExample and check whether ( lazabs.GlobalParameters.get.plainCEX || lazabs.GlobalParameters.get.simplifiedCEX) is true if that is preferred?
Check for needFullCEX instead of plainCEX
3 participants
This commit reduces the time to get an answer when the result is unsat. Generating a counterexample can also cause a stackoverflow in some cases.
Results below for running the symex engine on this file: https://github.com/chc-comp/aeval-unsafe/blob/de86ef1051b1c521b8c04f5c30c13f417d339529/s_split_01.smt2
Before changes:
% command time ./eld -sym:bfs s_split_01_equivalent.smt2
unsat
72,82 real 93,15 user 1,98 sys
After changes:
% command time ./eld -sym:bfs s_split_01_equivalent.smt2
unsat
3,61 real 6,94 user 0,27 sys