This project has moved and is read-only. For the latest updates, please go here.


CADE encoding not working


If command run_symdiff_bpl.cmd v1 v2 /rvt /opts:" -usemutual -useMutualSummariesAsAxioms -freeContracts " under SymDiff/Test/resilience/approx_feb_2015/examples/control/arr1 directory,

an error message shows,

"Fatal error: SymDiff failed with exception Collection was modified; enumeration operation may not execute."
Closed Aug 20, 2015 at 10:58 PM by shuvendu
closed for now


shuvendu wrote Aug 19, 2015 at 2:06 AM

The option -useMutualSummariesAsAxioms is less tested.

For now,

run_symdiff_bpl.cmd v1 v2 /rvt /opts:"-usemutual -asserts -useMutualSummariesAsAxioms -freeContracts"

will generate a valid mergedProgSingle.bpl file.

Guoanshisb wrote Aug 19, 2015 at 2:41 AM

It is fixed.