Skip to content

Endless recursion in SMGExpressionEvaluator

SMGExpressionEvaluator adds the state 2357 paired with the unknown value multiple times. Then it never empties the queue of pairs to evaluate.

Example: scripts/cpa.sh -heap 4000M -benchmark -setprop cpa.smg.runtimeCheck=NONE -setprop log.consoleLevel=OFF -smg-ldv -timelimit 60s -stats -spec test/programs/benchmarks/properties/valid-memsafety.prp -64 test/programs/benchmarks/busybox-1.22.0/basename-1.i

Maybe all these evaluating methods should return sets instead of lists to avoid duplicates in the queue?