title: Quantifier Elimination for LIA in Z3 via C/C++ API
body: <p>I would like to use Z3 for eliminating quantifiers in linear integer arithmetic formulas  via C/C++ API. Consider a simple example: Exists (x) ( x &lt;= y &amp; y &lt;= 2*x). A quantifier-free 
   formula with the same models is y >= 0.</p>
  
  <p>I tried to do it this way: </p>
  
  <pre><code>   context ctx;
     ctx.set("ELIM_QUANTIFIERS", "true");
     expr x = ctx.int_const("x"); 
     expr y = ctx.int_const("y"); 
     expr sub_expr = (x &lt;= y)  &amp;&amp; (y &lt;= 2*x);
  
     Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                                    0, {}, // patterns don't seem to make sense here.
                                    sub_expr); //No C++ API for quantifiers :(
     qf = Z3_simplify(ctx, qf);
     cout &lt;&lt; Z3_ast_to_string(ctx, qf);
  </code></pre>
  
  <p>what I get is </p>
  
  <blockquote>
    <p>(exists ((x Int) (and (&lt;=  x  y) (&lt;= y (* 2 x))))</p>
  </blockquote>
  
  <p>whereas I'd like to obtain something like </p>
  
  <blockquote>
    <p>(&lt;= 0 y)</p>
  </blockquote>
  
  <p>Is there a possibility to get it with Z3? 
  Many thanks in advance. </p>