search

sosy-lab / java-smt

JavaSMT - Unified Java API for SMT solvers.
Apache License 2.0
182 stars 46 forks source link

Assertion in SMTInterpol #200

Closed kfriedberger closed 4 years ago

kfriedberger commented 4 years ago

There is an assertion in SMTInterpol that does not appear when using the plain SMTLIB dump with the library.

Possible steps to do:

Source:

https://buildbot.sosy-lab.org/cpachecker/results/ldv-unsafes/00719.-r34451_integration-ldv-unsafes.2020-07-16_14-35-13.logfiles/linux-3.12-rc1.tar.xz-100_1a-drivers--tty--nozomi.ko-ldv_main0.cil.out.yml.log

Cmdline in CPAchecker (r34451):

scripts/cpa.sh -noout -heap 3000M -setprop statistics.memory=true -ldv-bam -timelimit 180s -stats \
-spec test/programs/ldv-benchmarks/properties/unreach-label.prp \
test/programs/ldv-benchmarks/unsafes/100_1a/linux-3.12-rc1/linux-3.12-rc1.tar.xz-100_1a-drivers--tty--nozomi.ko-ldv_main0.cil.out.c

Stacktrace:

Exception in thread "main" java.lang.AssertionError
at de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.map(Model.java:253)
at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ModelBuilder.add(ModelBuilder.java:135)
at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ModelBuilder.fillInFunctions(ModelBuilder.java:125)
at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.ModelBuilder.(ModelBuilder.java:70)
at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CClosure.fillInModel(CClosure.java:1204)
at de.uni_freiburg.informatik.ultimate.smtinterpol.model.Model.(Model.java:121)
at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.buildModel(SMTInterpol.java:1128)
at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getModel(SMTInterpol.java:1006)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolEnvironment.getModel(SmtInterpolEnvironment.java:339)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolAbstractProver.getModel(SmtInterpolAbstractProver.java:87)
at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolAbstractProver.getModel(SmtInterpolAbstractProver.java:34)
at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:79)
at org.sosy_lab.java_smt.basicimpl.reusableStack.ReusableStackAbstractProver.getModelAssignments(ReusableStackAbstractProver.java:81)
at org.sosy_lab.java_smt.basicimpl.reusableStack.ReusableStackInterpolatingProver.getModelAssignments(ReusableStackInterpolatingProver.java:17)
at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.getModelAssignments(BasicProverWithAssumptionsWrapper.java:83)
at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:66)
at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.getErrorPath(InterpolationManager.java:698)
at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager$Interpolator.buildCounterexampleTrace(InterpolationManager.java:846)
at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace0(InterpolationManager.java:330)
at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.lambda$buildCounterexampleTrace$0(InterpolationManager.java:271)
at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.callWithTimelimit(InterpolationManager.java:280)
at org.sosy_lab.cpachecker.util.predicates.interpolation.InterpolationManager.buildCounterexampleTrace(InterpolationManager.java:270)
at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performInterpolatingRefinement(PredicateCPARefiner.java:420)
at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.checkCounterexample(PredicateCPARefiner.java:411)
at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:281)
at org.sosy_lab.cpachecker.util.refinement.DelegatingARGBasedRefiner.performRefinementForPath(DelegatingARGBasedRefiner.java:80)
at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:157)
at org.sosy_lab.cpachecker.cpa.bam.BAMBasedRefiner.performRefinementForPath(BAMBasedRefiner.java:96)
at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:102)
at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:294)
at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:240)
at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:532)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:399)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:167)
kfriedberger commented 4 years ago

This exception seems to no longer appear with SMTInterpol 2.5-715-g3a7695dc. The previously given cmdline for CPAchecker finishes without problems.

kfriedberger commented 4 years ago

The bug no longer appears in CPAchecker r34849. Lets close this issue.