bug

[c-cube]

smbc @ f36a3af4bbd1e76bc85b00957224eb7ee9d1db58
msat @ 03dd2f9
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]

Seems ok. But:

smbc @ 8a953d05a3a33a37d68eb13494cbbe95e0efcba7
msat @ 03dd2f9
./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.