Aborted (core dumped)

[Fuhj-better]

The ebmc only works without crashing when using the default engine, Minisat. It crashes when using other engines.For example, using Yices results in a crash, and the same outcome occurs with other engines as well.

root@?:~# ebmc $SVWin/fifo1.sv --top fifo --bound 10  --yices
Parsing /mnt/c/Users/huijie/Desktop/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:1216 function: convert_expr
Condition: concatenation over a single operand should have matching types
Reason: expr.type() == expr.operands().front().type()
Backtrace:
ebmc(+0x16fb62) [0x56026c515b62]
ebmc(+0x1708dd) [0x56026c5168dd]
ebmc(+0xad929) [0x56026c453929]
ebmc(+0x191256) [0x56026c537256]
ebmc(+0x2eb647) [0x56026c691647]
ebmc(+0x2ececa) [0x56026c692eca]
ebmc(+0x2e7b21) [0x56026c68db21]
ebmc(+0x2e91a0) [0x56026c68f1a0]
ebmc(+0x300ca3) [0x56026c6a6ca3]
ebmc(+0x30104d) [0x56026c6a704d]
ebmc(+0x36c423) [0x56026c712423]
ebmc(+0xbda35) [0x56026c463a35]
ebmc(+0xf6308) [0x56026c49c308]
ebmc(+0xfa965) [0x56026c4a0965]
ebmc(+0xcd4e6) [0x56026c4734e6]
ebmc(+0x9da0f) [0x56026c443a0f]
ebmc(+0x9ba69) [0x56026c441a69]
/lib/x86_64-linux-gnu/libc.so.6(+0x29d90) [0x7f5e72619d90]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0x80) [0x7f5e72619e40]
ebmc(+0xa63f5) [0x56026c44c3f5]

Diagnostics:
<< EXTRA DIAGNOSTICS >>
concatenation
  * type: unsignedbv
      * width: 1
  * #source_location:
    * file: /SV/SVATEST/src/rtl/fifo1.sv
    * line: 89
    * working_directory: /root
  0: symbol
      * type: bool
      * identifier: Verilog::fifo.in_hsk@0
<< END EXTRA DIAGNOSTICS >>

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

Here is the code.

fifo1.zip