How to use boolector for SMT backend

[zilongwang123]

I want to verify property encoded in SVA to smt using write_smt2 and verify it using SMT backend with boolector.
The verilog code

module test(input clk, input rst, output y);
  reg [2:0] state;
  always @(posedge clk) begin
    if (rst || state == 3) begin
      state <= 0;
    end else begin
      assert(state < 3);
      state <= state + 1;
    end
  end
  assign y = state[2];
  assert property (y !== 1'b1);
endmodule

The script I used:

     read_verilog -sv fsm.v
    proc
    opt
    dffunmap
    write_smt2 fsm.smt

The command for yosys-smtbmc:
yosys-smtbme -s boolector fsm.smt

The result:
BrokenPipeError: [Errno 32] Broken pipe

[KrystalDelusion]

It works fine for me, do you have boolector installed? Try boolector --version