[Symex] Only generate counterexample when the user asks for it #67
Conversation
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.
| @@ -80,7 +80,8 @@ trait ConstraintSimplifierUsingConjunctEliminator extends ConstraintSimplifier { | |||
| symex_sf.reducer(Conjunction.TRUE)(constraint) | |||
| 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.
| @@ -56,6 +56,10 @@ abstract class Symex[CC](iClauses: Iterable[CC])( | |||
| import Symex._ | |||
|
|
|||
| 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
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