Z3 C++ API: set parameter for tactic -

i'm using z3 c++ api of smt solver , i'd change parameters of "ctx-solver-simplify". don't know how input them tactic. tried:

z3::context c;  c.set("arith_lhs",false); c.set("eq2ineq",true); 

and

z3::params params(c); params.set("arith_lhs",true); params.set("eq2ineq",true); 

example code:

z3::expr x = c.int_const("x"); z3::expr cond1 = !(x==4);  z3::goal g(c); g.add(cond1);  z3::tactic t(c, "ctx-solver-simplify"); z3::apply_result r = t(g); 

the result

(goal (not (= x 4))) 

and not

(goal ,  (< x 4) (> x 4) 

same applies arith_lhs. help? thanks!

change: z3::tactic t(c, "ctx-solver-simplify"); z3::tactic t = with(z3::tactic(c, "simplify"), params);

this instruct z3 apply simplify tactic selected parameters. in smt-lib api accomplished "using-params" combinator. got above c++ equivalent example.cpp shipped z3 source.

so there 2 problems: (1) need tell z3 apply given tactic selected parameters. (2) ctx-solver-simplify tactic not have eq2ineq option. other tactics do, though, including simplify.