data/full_repos/permissive/441359809/src/yosys/examples/smtbmc/demo2.v
data/verilator_xmls/3b78ed17-dcb3-4a10-9048-e8a6a7d24d31.xml
module demo2(input clk, input [4:0] addr, output reg [31:0] data);
	reg [31:0] mem [0:31];
	always @(negedge clk)
		data <= mem[addr];

	reg [31:0] used_addr = 0;
	reg [31:0] used_dbits = 0;
	reg initstate = 1;

	always @(posedge clk) begin
		initstate <= 0;
		`assume(!used_addr[addr]);
		used_addr[addr] <= 1;
		if (!initstate) begin
			`assume(data != 0);
			`assume((used_dbits & data) == 0);
			used_dbits <= used_dbits | data;
		end
	end
endmodule
module demo2(input clk, input [4:0] addr, output reg [31:0] data);

	reg [31:0] mem [0:31];
	always @(negedge clk)
		data <= mem[addr];

	reg [31:0] used_addr = 0;
	reg [31:0] used_dbits = 0;
	reg initstate = 1;

	always @(posedge clk) begin
		initstate <= 0;
		`assume(!used_addr[addr]);
		used_addr[addr] <= 1;
		if (!initstate) begin
			`assume(data != 0);
			`assume((used_dbits & data) == 0);
			used_dbits <= used_dbits | data;
		end
	end
endmodule