Too many asserts are discharged to the SMT solver

[krtab]

There's a bug regarding the Ptr type returned by owi_alloc. I just ran this locally, and with -w 8 owi is making 8200 calls to the solver, totaling 34s in the solver. This means that the expressions in owi_assert, i.e., stuff like this:

calling func : func owi_assert
stack        : [  ]
running instr: local.get 0
stack        : [ (i32.of_bool (i32.eq (i32.rem (Ptr (i32 8390672) (i32 0)) (i32 1)) (i32 0))) ]

Is being discharged to the solver instead of being solved concretely

Originally posted by @filipeom in https://github.com/OCamlPro/owi/issues/118#issuecomment-1904588321

[krtab]

Constant booleans are not passed to the solver currently https://github.com/OCamlPro/owi/blob/c3ee732a5992ca42e3aaa51b4a46ba0306eeafd2/src/symbolic_choice.ml#L11-L18

So I think this boils down to having enough reductions implemented in encoding