Issues related to options in smt module

[r0ayane]

Hi, z3 gives unsat for the following instance.

$ cat test.smt
(set-option :smt.phase_selection 1)
(set-option :smt.arith.propagate_eqs false)
(set-option :smt.arith.eager_eq_axioms false)
(declare-fun i1 () Int)
(declare-fun str1 () String)
(assert (<= 32 (str.len str1)))
(minimize i1)
(check-sat)
$ z3 test.smt
unsat

However, z3 gives sat for the same instance without options.

$ cat no-options.smt
(declare-fun i1 () Int)
(declare-fun str1 () String)
(assert (<= 32 (str.len str1)))
(minimize i1)
(check-sat)
$ z3 no-options.smt
sat

Version: z3 4.13.0 3049f57