Soundness issue with push and pop

[Stevendeo]

Push and pop have a serious soundness issue.

File prelude.ae:

(* This is conceptually [<=] but we don't let Alt-Ergo know *)
logic my_leq : real, real -> bool

theory My_theory extends FPA =
  axiom triggers :
    forall x : real [ int_floor(x) ]. my_leq(real_of_int(int_floor(x)), x)
end

File test.smt2

(set-logic ALL)

(declare-const x Real)

(check-sat)

(push 1)
  (assert (not (my_leq (to_real (to_int x)) x)))
  (push 1)  (pop 1)
(pop 1)

(check-sat)

Alt-ergo returns unknown for the first check-sat and unsat for the second. The second is definitely not unsat, it should actually be the same than the first check-sat.

If we remove the line (push 1) (pop 1) , then alt-ergo answers soundly.

[bclement-ocp]

Seems to have been introduced here: the frontend is pushing twice since #936 .