Gbury / mSAT

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

vec.get error #25

Closed c-cube closed 4 years ago

c-cube commented 4 years ago

using https://github.com/c-cube/sidekick at commit 0b283a384d4f276e2128c1eeb0817b7f8cf17636 the following error is raised within msat:

./sidekick tests/sat/typed_v3l60005.cvc.smt2 --bt
invalid argument:
vec.get
Raised at file "pervasives.ml", line 33, characters 20-45
Called from file "src/core/Vec.ml" (inlined), line 54, characters 29-50
Called from file "src/core/Internal.ml", line 1413, characters 16-40
Called from file "src/core/Internal.ml", line 1503, characters 13-29
Called from file "src/core/Internal.ml", line 1562, characters 10-40
Called from file "src/core/Internal.ml", line 1578, characters 6-22
Called from file "src/core/Internal.ml" (inlined), line 1582, characters 50-67
Called from file "src/core/Internal.ml", line 2035, characters 16-32
Called from file "src/core/Internal.ml", line 2162, characters 6-15
Called from file "src/msat-solver/Sidekick_msat_solver.ml", line 607, characters 12-55
Called from file "src/smtlib/Process.ml", line 155, characters 4-44
Called from file "src/smtlib/Process.ml", line 229, characters 6-130
Called from file "src/core/CCResult.ml", line 239, characters 22-30
Called from file "list.ml", line 100, characters 12-15
Called from file "src/core/CCResult.ml", line 238, characters 4-125
Called from file "src/main/main.ml", line 184, characters 15-21
c-cube commented 4 years ago

actually fixed on master -_-