read_verilog <<EOT
module gold(
	input wire [7:0] a,
	input wire [7:0] b,
	output wire [7:0] c
);

wire [7:0] b_neg;
assign b_neg = -b;
assign c = a + b_neg;
endmodule

module gate(
	input wire [7:0] a,
	input wire [7:0] b,
	output wire [7:0] c
);

wire [7:0] b_neg;
assign b_neg = ~b + 1;
assign c = a + b_neg;
endmodule

EOT

equiv_make -make_assert gold gate miter

select -assert-count 0 t:$equiv
select -assert-count 2 t:$assert

prep -top miter
sat -prove-asserts -verify
