search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
198 stars 41 forks source link

Array theory solver does not yet support write-chains connecting two different constant arrays #407

Open Heizmann opened 5 years ago

Heizmann commented 5 years ago 
    Input:svcomp/array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i Settings:settings/svcomp2017/automizer/svcomp-DerefFreeMemtrack-32bit-Automizer_Bitvector.epf Toolchain:toolchains/AutomizerC.xml
        ExpectedResult: SAFE UltimateResult: EXCEPTION_OR_ERROR   [de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Array theory solver does not yet support write-chains connecting two different constant arrays: de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.TraceCheck.<init>(TraceCheck.java:239)]

Just FYI, don't know if this can be implemented easily. Occurs in ~5-10% of memsafety benchmarks. Maybe we can simplify equalities on const-arrays immediately to reduce the problem.

Heizmann commented 5 years ago

This probably means that we have to add this error message to the TraceChecker, in order to let it continue with the next solver.

danieldietsch commented 5 years ago

For reference:

The solver in question is cvc4 1.7-prerelease [git master 391ab9df] , strategy is WOLF.

It also happens with settings default/automizer/svcomp-DerefFreeMemtrack-32bit-Automizer_Bitvector.epf.

danieldietsch commented 5 years ago

We do not crash anymore if it occurs in a strategy. But I think we should keep the ticket open so that we can investigate @Heizmann 's proposal:

Maybe we can simplify equalities on const-arrays immediately to reduce the problem.