Counterexample about array read

36 views

Skip to first unread message

Hong Hu

unread,

Dec 5, 2013, 2:40:13 AM12/5/13

to stp-...@googlegroups.com

Hi,

I'm trying to use stp to my formulas, especially for generating a counterexample. However I found some unnecessary assertion on the array when using array read with variable index.

Here is the formula I want to solve:

mem : ARRAY BITVECTOR(64) OF BITVECTOR(8);
tmp_index : BITVECTOR(32);

ASSERT(tmp_index = 0hexbffff7d4);
ASSERT(0hex01 =
(LET mem_1 =
(mem WITH [0hex00000000bffff7d4] := 0hex01)
IN
mem_1[0hex00000000 @ tmp_index]));

QUERY(FALSE);
COUNTEREXAMPLE;

The output of stp solver is :

ASSERT( mem[0hex00000000BFFFF7D4] = 0x00 );
ASSERT( tmp_index = 0xBFFFF7D4 );
Invalid.

However, the first assertion on mem is not necessary since there will be a initialization line "(mem WITH [0hex00000000bffff7d4] := 0hex01)" to overwrite it.

Is it possible to remove such unnecessary assertion from the counterexample so that I can focus on other assertions?