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 #118 (comment)

[krtab]

Constant booleans are not passed to the solver currently

owi/src/symbolic_choice.ml

Lines 11 to 18 in c3ee732

	let check sym_bool thread =
	let (S (solver_module, solver)) = Thread.solver thread in
	let pc = Thread.pc thread in
	let no = S.Bool.not sym_bool in
	let no = Expr.simplify no in
	match no.e with
	| Val True -> false
	| Val False -> true

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