Unexpected unsat from check() when using push/pop with assertions from parse_smt2_string

[benquike]

I've encountered unexpected behavior when using the incremental solver (push/pop) on a set of assertions that were parsed from an SMT-LIB2 string.

A problem that is clearly satisfiable returns unsat (or unknown) when solver.check() is called within a push/pop block. However, if the push() and pop() calls are removed, the solver correctly returns sat. This suggests a potential issue with how parsed assertions interact with the incremental solving context.

The following self-contained Python script demonstrates the issue. The SMT logic defines a function that should be satisfiable for the input arg1 == 2.

import z3

smt_code = """
(declare-fun __example_0__example () (Array (_ BitVec 8) (_ BitVec 8)))
(assert (let ((a!1 (lambda ((x (_ BitVec 8)))
                (let ((a!1 (bvredor (bvxor (bvredor (bvxor x #x00)) #b0))))
                (ite (not (= (bvnot a!1) #b0)) #x01 #x04)))))
(= __example_0__example a!1)))

(declare-const arg1 (_ BitVec 8))
(declare-const result (_ BitVec 8))
(assert (= result (select __example_0__example arg1)))
"""
   
assertions = z3.parse_smt2_string(smt_code)
 
# extract arg1 from `(assert (= result (select __example_0__example arg1)))` in the smt code
arg1 = assertions[1].arg(1).children()[1]

result_var = assertions[1].arg(0)

print(result_var)

solver = z3.Solver()
# print(solver)
solver.add(assertions)
# if the push pop is commented out, the solver could find a solution
solver.push()
solver.add(arg1 == 2)


if solver.check() == z3.sat:
  print(solver)
  model = solver.model()
  print(f'{model[arg1]=}')
  print(f'{model[result_var]=}')
  print('\n ✅ --- Found a model ---')
else:
  print('❌ Solver did not find a solution.')

solver.pop()

Expected Behavior:
The script should successfully find a model where arg1 = 2. The expected output is:

--- Performing check within push/pop block ---
✅ SAT: Solver found a solution as expected.
Actual Behavior:
The script reports that a solution could not be found. The actual output is:

--- Performing check within push/pop block ---
❌ UNSAT/UNKNOWN: Solver failed to find a solution.
The core issue is that the problem is satisfiable, but solver.check() fails only when used incrementally on the parsed assertions.

Could you please clarify if this is intended behavior or if this might be a bug?

[benquike]

moved to #7965