Assertion `!(pointer && arithmetics)' failed

[blizzard4591]

It seems that 2LS does not support a pointer to an array, if the pointer is not pointing to the first element. Attached you can find our program under test which produced this output:

./2ls --graphml-witness witness.graphml --propertyfile ../../custom-benchmarks/Wrappers/Wrapper_AP/reach.prp --32 ../../custom-benchmarks/Wrappers/Wrapper_AP/Req1_Prop1_Batch0Wrapper_AP.c

--------------------------------------------------------------------------------

./2ls: line 11:    19 Aborted                 $TOOL_BINARY --graphml-witness $LOG.witness --object-bits $OBJ_BITS $PROPERTY $LOG.bin >> $LOG.ok 2>&1
2LS version 0.9.6-sv-comp22
Reading GOTO program from file
Reading: /tmp/2LS-log.c4mm80.bin
Generating GOTO Program
Adding CPROVER library
file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module Req1_Prop1_Batch0Wrapper_AP file <built-in-additions> line 24
8388608u
ignoring new value in module <built-in-library> file <built-in-additions> line 24
1048576u
Function Pointer Removal
Performing full inlining
Generic Property Instrumentation
2ls-binary: ssa_value_set.cpp:328: void ssa_value_domaint::assign_rhs_rec(ssa_value_domaint::valuest&, const exprt&, const namespacet&, bool, unsigned int) const: Assertion `!(pointer && arithmetics)' failed.
UNKNOWN

2LS_Issue.zip

[viktormalik]

Indeed, 2LS currently doesn't handle pointer arithmetics, so we only allow pointers to the beginning of a memory object.