qbfsat_solnfile1.disable

logger -expect log "Specializing \\demo9 from file with \\h = 8'b00000010." 1

read_verilog -formal <<EOT
module demo9(a, b, trigger);
	input [3:0] a;
	input [3:0] b;
	wire [7:0] i = {a, b};
	(* maximize *) wire [7:0] h;
       	assign h = $anyconst;

	wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011);
	output trigger = (t0 > h) && (h < 8'b00000100);

	always @* begin
		assume(trigger == 1'b1);
		cover(1);
	end
endmodule
EOT
proc; techmap
prep -top demo9 -nordff
qbfsat -specialize-from-file ../qbf_solution1.txt