search

Gbury / mSAT

A modular sat/smt solver with proof output.
https://gbury.github.io/mSAT/
Apache License 2.0
95 stars 8 forks source link

invalid_argument #5

Closed c-cube closed 7 years ago

c-cube commented 7 years ago

with smbc @ 71faccb8e0607c4e05c83ba1041b16be45abd797

./smbc.native --debug 5 --check examples/rev.lisp --depth-step 1 --backtrace

I get

Fatal error: exception Invalid_argument("Sparse_vec.set") Raised at file "pervasives.ml", line 31, characters 25-45 Called from file "src/util/sparse_vec.ml", line 64, characters 29-57 Called from file "src/core/internal.ml", line 218, characters 6-43 Called from file "src/core/internal.ml", line 420, characters 12-47 Called from file "src/core/internal.ml", line 1145, characters 6-33 Called from file "src/Solver.ml", line 2810, characters 18-41 Called from file "src/smbc.ml", line 55, characters 12-51 Called from file "src/smbc.ml", line 165, characters 2-19

Gbury commented 7 years ago

Which version of msat ? The current master has a comment on line 218 in src/core/internal.ml.

c-cube commented 7 years ago

0.4.1

Gbury commented 7 years ago

Fixed in e6f3e79acc3e44af4b2fd4daba7e22830fbc13ad