BAM: StackOverflow
Original issue created by @koosa on 2017-03-14 at 15:02:38, last modified on 2017-03-20 at 01:15:04
#################################
CPAchecker Trunk: 24551
Files: -> recursive-simple/fibo_15_false-unreach-call.c -> recursive-simple/fibo_2calls_15_false-unreach-call.c -> recursive-simple/id_o1000_false-unreach-call.c
Fastest (slightly): -> recursive-simple/id_o1000_false-unreach-call.c
scripts/cpa.sh -heap 6000M -witness-validation -disable-java-assertions -heap 10000m -spec test/results/integration-witness-generation.logfiles/witness-generation.fibo_15_false-unreach-call.c.files/output/witness.graphml.gz -setprop cpa.callstack.skipVoidRecursion=false -timelimit 90s -stats -spec test/programs/benchmarks/ReachSafety.prp test/programs/benchmarks/recursive-simple/fibo_15_false-unreach-call.c
#################################
Stacktrace:
Using predicate analysis with MathSAT5 version 5.3.14 (0b98b661254c) (Nov 17 2016 10:59:45, gmp 5.1.3, gcc 4.8.5, 64-bit) and JFactory 1.21. (Analysis2:BAMPredicateCPA:PredicateCPA.<init>, INFO)
Using refinement for predicate analysis with BAMPredicateAbstractionRefinementStrategy strategy. (Analysis2:BAMPredicateCPA:PredicateCPARefiner.<init>, INFO)
Exception in thread "main" java.lang.StackOverflowError
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.makeVariable(CtoFormulaConverter.java:429)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.ExpressionToFormulaVisitor.visit(ExpressionToFormulaVisitor.java:395)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.ExpressionToFormulaVisitor.visit(ExpressionToFormulaVisitor.java:73)
at org.sosy_lab.cpachecker.cfa.ast.c.CIdExpression.accept(CIdExpression.java:66)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.buildTerm(CtoFormulaConverter.java:1363)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.makeAssignment(CtoFormulaConverter.java:1319)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.makeAssignment(CtoFormulaConverter.java:1277)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.addParameterConstraints(CtoFormulaConverter.java:893)
at org.sosy_lab.cpachecker.util.predicates.pathformula.ctoformula.CtoFormulaConverter.makeAnd(CtoFormulaConverter.java:814)
at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.makeAnd(PathFormulaManagerImpl.java:203)
at org.sosy_lab.cpachecker.util.predicates.pathformula.PathFormulaManagerImpl.makeAnd(PathFormulaManagerImpl.java:255)
at org.sosy_lab.cpachecker.util.predicates.pathformula.CachingPathFormulaManager.makeAnd(CachingPathFormulaManager.java:102)
at org.sosy_lab.cpachecker.cpa.predicate.PredicateTransferRelation.convertEdgeToPathFormula(PredicateTransferRelation.java:231)
at org.sosy_lab.cpachecker.cpa.predicate.PredicateTransferRelation.getAbstractSuccessorsForEdge(PredicateTransferRelation.java:152)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callTransferRelation(CompositeTransferRelation.java:267)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:237)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:175)
at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:108)
at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:61)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.getAbstractSuccessorsWithoutWrapping(BAMTransferRelation.java:165)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelationWithFixPointForRecursion.getAbstractSuccessorsWithoutWrapping(BAMTransferRelationWithFixPointForRecursion.java:100)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.getAbstractSuccessors(BAMTransferRelation.java:114)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:299)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:254)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:220)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.performCompositeAnalysisWithCPAAlgorithm(BAMTransferRelation.java:521)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.getReducedResult(BAMTransferRelation.java:462)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.analyseBlockAndExpand(BAMTransferRelation.java:337)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelationWithFixPointForRecursion.analyseBlockAndExpandForRecursion(BAMTransferRelationWithFixPointForRecursion.java:348)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelationWithFixPointForRecursion.analyseBlockAndExpand(BAMTransferRelationWithFixPointForRecursion.java:293)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.doRecursiveAnalysis(BAMTransferRelation.java:290)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.getAbstractSuccessorsWithoutWrapping(BAMTransferRelation.java:151)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelationWithFixPointForRecursion.getAbstractSuccessorsWithoutWrapping(BAMTransferRelationWithFixPointForRecursion.java:100)
at org.sosy_lab.cpachecker.cpa.bam.BAMTransferRelation.getAbstractSuccessors(BAMTransferRelation.java:114)