1

Closed

CADE encoding not working

description

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 9:58 PM by shuvendu
closed for now

comments

shuvendu wrote Aug 19, 2015 at 1: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 1:41 AM

It is fixed.