Aborted (core dumped)

[Fuhj-better]

After modifying the code, changing from

assign add_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_head_reg) & {INFLIGHT{in_hsk}};
assign clr_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_tail_reg) & {INFLIGHT{out_hsk}};

to

assign add_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_head_reg) & {{INFLIGHT-1{1'b1}},in_hsk};
assign clr_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_tail_reg) & {{INFLIGHT-1{1'b1}},out_hsk};

(even though the original code was correct as mentioned in #977 ), a new crash message now appears, and detailed crash information cannot be displayed. Only the default engine Minisat can run normally and any other engines will fail and abort.

Here is the error message.

root@:~# ebmc $SVWin/fifo1.sv --top fifo --bound 10  --cvc4
Parsing /SV/SVATEST/src/rtl/fifo1.sv
Converting
Type-checking Verilog::fifo
Generating Decision Problem
--- begin invariant violation report ---
Invariant check failed
File: smt2/smt2_conv.cpp:2582 function: convert_expr
Condition: smt2_convt::convert_expr should not be applied to unsupported expression       
Reason: false
Backtrace:
ebmc(+0x16fb62) [0x565049560b62]
ebmc(+0x1708dd) [0x5650495618dd]
ebmc(+0xad929) [0x56504949e929]
ebmc(+0x308176) [0x5650496f9176]
ebmc(+0x2ea40d) [0x5650496db40d]
ebmc(+0x2e91a0) [0x5650496da1a0]
ebmc(+0x300ca3) [0x5650496f1ca3]
ebmc(+0x30104d) [0x5650496f204d]
ebmc(+0x36c423) [0x56504975d423]
ebmc(+0xbda35) [0x5650494aea35]
ebmc(+0xf6308) [0x5650494e7308]
ebmc(+0xfa965) [0x5650494eb965]
ebmc(+0xcd4e6) [0x5650494be4e6]
ebmc(+0x9da0f) [0x56504948ea0f]
ebmc(+0x9ba69) [0x56504948ca69]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f526e75dd90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f526e75de40]
ebmc(+0xa63f5) [0x5650494973f5]

Diagnostics:
<< EXTRA DIAGNOSTICS >>
reduction_or
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Aborted (core dumped)

Here is the complete code.

fifo1.zip

[Fuhj-better]

After modifying the code, changing from

assign add_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_head_reg) & {INFLIGHT{in_hsk}};
assign clr_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_tail_reg) & {INFLIGHT{out_hsk}};

to

assign add_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_head_reg) & {{INFLIGHT-1{1'b1}},in_hsk};
assign clr_buffer = ({{INFLIGHT-1{1'b0}}, 1'b1} << buffer_tail_reg) & {{INFLIGHT-1{1'b1}},out_hsk};

(even though the original code was correct as mentioned in #977 ), a new crash message now appears, and detailed crash information cannot be displayed. Only the default engine Minisat can run normally and any other engines will fail and abort.

Here is the error message.

root@:~# ebmc $SVWin/fifo1.sv --top fifo --bound 10  --cvc4
Parsing /SV/SVATEST/src/rtl/fifo1.sv
Converting
Type-checking Verilog::fifo
Generating Decision Problem
--- begin invariant violation report ---
Invariant check failed
File: smt2/smt2_conv.cpp:2582 function: convert_expr
Condition: smt2_convt::convert_expr should not be applied to unsupported expression       
Reason: false
Backtrace:
ebmc(+0x16fb62) [0x565049560b62]
ebmc(+0x1708dd) [0x5650495618dd]
ebmc(+0xad929) [0x56504949e929]
ebmc(+0x308176) [0x5650496f9176]
ebmc(+0x2ea40d) [0x5650496db40d]
ebmc(+0x2e91a0) [0x5650496da1a0]
ebmc(+0x300ca3) [0x5650496f1ca3]
ebmc(+0x30104d) [0x5650496f204d]
ebmc(+0x36c423) [0x56504975d423]
ebmc(+0xbda35) [0x5650494aea35]
ebmc(+0xf6308) [0x5650494e7308]
ebmc(+0xfa965) [0x5650494eb965]
ebmc(+0xcd4e6) [0x5650494be4e6]
ebmc(+0x9da0f) [0x56504948ea0f]
ebmc(+0x9ba69) [0x56504948ca69]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f526e75dd90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f526e75de40]
ebmc(+0xa63f5) [0x5650494973f5]

Diagnostics:
<< EXTRA DIAGNOSTICS >>
reduction_or
<< END EXTRA DIAGNOSTICS >>

--- end invariant violation report ---
Aborted (core dumped)

Here is the complete code.

fifo1.zip

Is there no solution to this problem?