qe2 introduces a non-linear term (a product of two variables) when eliminating quantifiers from a linear (LIA) formula

[daniel-larraz]

Summary

Applying the qe2 tactic to a purely linear integer-arithmetic formula produces a goal that contains a product of two variables (x * x1). The classic qe tactic (and qe-light) return a linear result for the same input. The qe2 result is logically equivalent to the linear one, so this does not appear to be a soundness problem — but the non-linear term is surprising for a LIA input and breaks downstream consumers that assume quantifier elimination over LIA stays within linear arithmetic (in our case, a QF_LIA solver instance rejects the resulting atom with "logic does not support nonlinear arithmetic").

Is this expected behavior for qe2, or a bug? Is there a way to keep qe2's output within the linear fragment (short of using qe instead)?

Version

Reproduces on 4.15.3, 4.16.0, and 5.0.0 (latest release), Linux x64.

Reproducer

(declare-const x Int)
(declare-const x1 Int)
(declare-const y Int)
(assert (forall ((X Int))
  (or (= X 0) (distinct 0 y) (distinct 0 (+ x x (ite (= x1 2) 0 1))))))
(apply qe2)

Everything in the input is linear: (+ x x (ite (= x1 2) 0 1)) is 2*x + ite(...), and X occurs only in (= X 0).

Actual output (qe2)

(goals
(goal
  (let ((a!1 (not (= (+ y (* (- 1) x x1)) 0))))
    (or (not (= x1 2)) a!1 (not (= y 0))))
  :precision precise :depth 1)
)

The atom (* (- 1) x x1) is -x*x1, a product of two variables. It appears that model-based projection uses x1's model value (2) and rewrites x + x as x * x1 instead of 2 * x.

For comparison, qe and qe-light stay linear

(apply qe):

(goal
  (let ((a!1 (= 0 (+ (* 2 x) (ite (= x1 2) 0 1)))))
    (not (and (= 0 y) a!1 true)))
  :precision precise :depth 1)

(apply qe-light) similarly yields (* 2 x).

The qe2 result is logically equivalent (not a soundness issue)

Let C be the linear result and Q the qe2 result; C xor Q is unsat:

(set-logic ALL)
(declare-const x Int) (declare-const x1 Int) (declare-const y Int)
(define-fun C () Bool (or (not (= y 0)) (not (= (+ (* 2 x) (ite (= x1 2) 0 1)) 0))))
(define-fun Q () Bool (or (not (= x1 2)) (not (= (+ y (* (- 1) x x1)) 0)) (not (= y 0))))
(assert (distinct C Q))
(check-sat)
; => unsat