Error in SMTConcretizer

[wadoon]

The attached gtt can be concretize if there are 50 repetition of row 2, but not with 100 reptitions.

Error message is unsatisfiable.

<?xml version="1.0" encoding="UTF-8"?><specification xmlns="http://formal.iti.kit.edu/stvs/logic/io/xml" comment="" isConcrete="false" name="Unnamed Specification">
<variables>
<ioVariable colwidth="100" data-type="INT" io="input" name="i"/>
<ioVariable colwidth="100" data-type="INT" io="output" name="o"/>
<freeVariable data-type="INT" default="&gt;6" name="variable"/>
</variables>
<rows>
<row comment="">
<duration>5</duration>
<cell>0</cell>
<cell>i</cell>
</row>
<row comment="">
<duration>100</duration>
<cell>=i[-1]+1</cell>
<cell>i</cell>
</row>
<row comment="">
<duration>2</duration>
<cell>=o[-1]/2</cell>
<cell>i</cell>
</row>
</rows>
</specification>

[matheus23]

This might be due to the unrolling of rows. Something seems to be done incorrectly when the duration of a row is greater than the maximum unrolling given in the user's config.

[wadoon]

As discussed on Friday, the logic should not be a minimum of the row duration and the global maximal duration but rather an if/then.

upperbound = 
  if upper(duration) == '-' then MAX_DURATION
                                       else upper(duration)