-
Notifications
You must be signed in to change notification settings - Fork 11
Open
Description
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
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels