allconst fails in weird ways

[Topi-ab]

This code gives different results, depending which coding style is adopted. Even though all 4 combinations should give equal results.

library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;

/*
	Commenting out between
	- t1 & t2
	- a1 & a2
	
	yields to following results:
	
	t1 & a1 enabled => fail
	t1 & a2 enabled => fail
	t2 & a1 enabled => fail
	t2 & a2 enabled => pass
*/

entity bug_2014_12_16 is
	port(
		clk_in: in std_logic
	);
end;

architecture formal of bug_2014_12_16 is
	attribute anyconst: boolean;
	attribute anyseq: boolean;
	attribute allconst: boolean;
	attribute allseq: boolean;
	
	constant LUT_IN_BITS: integer := 3;
	constant LUT_OUT_BITS: integer := 2;
	constant LUT_IN_PERMS: integer := 2**LUT_IN_BITS;
	
	-- t1 =>
	-- type lut_a is array(LUT_IN_PERMS-1 downto 0) of std_logic_vector(LUT_OUT_BITS-1 downto 0);
	
	-- t2 =>
	type lut_a is array(0 to LUT_IN_PERMS-1) of std_logic_vector(LUT_OUT_BITS-1 downto 0);
	
	signal lut_mem: lut_a;
	attribute anyconst of lut_mem: signal is true;
	
	signal lut_in: std_logic_vector(LUT_IN_BITS-1 downto 0);
	attribute allconst of lut_in: signal is true;
	
	signal lut_out: std_logic_vector(LUT_OUT_BITS-1 downto 0);
begin
	process(all)
	begin
		lut_out <= lut_mem(to_integer(unsigned(lut_in)));
	end process;
	
	default clock is rising_edge(clk_in);

	-- a1 =>
	-- a1: assume lut_out = "01";
	
	-- a2 =>
	a2: assume lut_out(1) = '0' and lut_out(0) = '1';
	
	cover {true};
end;

[tasks]
cover

[options]
mode cover
depth 1

[engines]
smtbmc --dumpsmt2 --progress --stbv z3

[script]
ghdl --std=08 bug_2014_12_16.vhdl -e bug_2014_12_16
prep -top bug_2014_12_16

[files]
bug_2014_12_16.vhdl