[go: up one dir, main page]

Crash in statistics with ImpactRefiner configuration

Original issue created by @PhilippWendler on 2012-12-07 at 07:42:36, last modified on 2012-12-17 at 12:29:12

The following crash happens with -predicateAnalysis-ImpactRefiner-ABEl when exporting the invariant:

Exception in thread "Thread-1" java.lang.UnsupportedOperationException
        at org.sosy_lab.cpachecker.util.predicates.SymbolicRegionManager.makeOr(SymbolicRegionManager.java:120)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPAStatistics.exportInvariants(PredicateCPAStatistics.java:273)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPAStatistics.printStatistics(PredicateCPAStatistics.java:156)
        at org.sosy_lab.cpachecker.core.MainCPAStatistics.printStatistics(MainCPAStatistics.java:294)
        at org.sosy_lab.cpachecker.core.CPAcheckerResult.printStatistics(CPAcheckerResult.java:80)
        at org.sosy_lab.cpachecker.cmdline.ShutdownHook.run(ShutdownHook.java:138)