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

bug #7

Closed c-cube closed 7 years ago

c-cube commented 7 years ago

smbc @ f36a3af4bbd1e76bc85b00957224eb7ee9d1db58 msat @ 03dd2f9e38c2ffdf6c443c1309abd80af13c9456 OCaml 4.03

doesn't work but should: ./smbc.native --debug 1 -t 60 --check examples/sorted.lisp almost similar: ./smbc.native --debug 1 -t 60 --check examples/sorted.lisp --depth-step 2

note: this works well ./smbc.native --debug 1 -t 60 --check examples/ty_infer.lisp

c-cube commented 7 years ago

Seems ok. But:

smbc @ 8a953d05a3a33a37d68eb13494cbbe95e0efcba7 msat @ 03dd2f9e38c2ffdf6c443c1309abd80af13c9456 ./smbc.native --debug 1 --check examples/long_rev_sum2.lisp --depth-step 5 triggers the same bug as before (get sat instead of unsat); it works --depth-step 1.