hopv/hoice

hoice crush with "-v -v -v"

naokikob opened this issue · 0 comments

hoice crushes for the benchmark:
https://github.com/chc-comp/rust-horn/blob/master/trees-1-append-safe.smt2
when run with "-v -v -v".

$ hoice -v -v -v trees-1-append-safe.smt2 
; Running top pre-processing
; running simplify
...
; looking for counterexamples in implication clauses (3)...
;   extracted 2 cexs
;   generating data from initial cex...
;     trying to break
;     (%append.0 (~mut<%Tree> (as %Tree-1 %Tree) (as %Tree-1 %Tree)) (as %Tree-1 %Tree)) (%sum.0 (as %Tree-1 %Tree) 0) (%sum.0 (as %Tree-1 %Tree) (- 1)) => false
thread 'main' panicked at src/teacher/assistant.rs:264:33:
index out of bounds: the len is 0 but the index is 1
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace