[Bug] The proof result differs between qbit_sequence_model and state_model!!!

[alan23273850]

#!/usr/bin/python3
import sys; sys.path.append('..')
import time
import numpy as np
from symqv.lib.expressions.qbit import Qbits
from symqv.lib.expressions.qbit import QbitVal
from symqv.lib.expressions.complex import ComplexVal
from symqv.lib.models.circuit import Circuit, Method
from symqv.lib.operations.gates import H, Z, CNOT
from z3 import And, Not

def prove_BVsingle(n: int):
    q = n+1
    qbits = Qbits([f'q{i}' for i in range(q)])
    circuit = Circuit(qbits,
                        [H(qbit) for qbit in qbits] +
                        [Z(qbits[-1])] +
                        [CNOT(qbit, qbits[-1]) for i, qbit in enumerate(qbits) if i % 2 == 0 and i < len(qbits)-1] +
                        [H(qbit) for qbit in qbits])
                    #   , delta=0.0001)
    print(circuit)
    initial_values = [(1, 0) for _ in range(q)]
    circuit.initialize(initial_values)
    # circuit.execute(True)

    # Build specification
    final_qbits = circuit.get_final_qbits()
    conjunction = []
    for i in range(n):
        conjunction.append(final_qbits[i].isclose(QbitVal(alpha = ComplexVal(i % 2), beta = ComplexVal(1 - (i % 2))), circuit.delta))
    conjunction.append(final_qbits[-1].isclose(QbitVal(alpha = ComplexVal(0), beta = ComplexVal(1)), circuit.delta))
    circuit.solver.add(Not(And(conjunction)))

    # Prove
    print(circuit.prove(method=Method.qbit_sequence_model))#, dump_smt_encoding=True, dump_solver_output=True))
    # The bug appears here! The result differs when n = 1.
    # Method.qbit_sequence_model => UNSAT, Method.state_model => SAT


if __name__ == "__main__":
    times = []

    for _ in range(1):
        start = time.time()
        prove_BVsingle(1)
        times.append(time.time() - start)

    print(f'Runtime:', np.mean(times))

The execution result of the above code would be

H(q0), H(q1), Z(q1), CNOT(q0, q1), H(q0), H(q1)
Starting solver...
Elapsed time 8.7015 seconds.
('unsat', {}, 8.70150876045227)
Runtime: 8.70550537109375

, but if we replace circuit.prove(method=Method.qbit_sequence_model) with circuit.prove(method=Method.state_model), the execution result becomes

H(q0), H(q1), Z(q1), CNOT(q0, q1), H(q0), H(q1)
Starting solver...

Elapsed time 0.7147 seconds.
('δ-sat with δ = 0.0001', OrderedDict([('psi_0_0', 1.0000 + 0.0000*I), ('psi_0_1', 0.0000 + 0.0000*I), ('psi_0_2', 0.0000 + 0.0000*I), ('psi_0_3', 0.0000 + 0.0000*I), ('psi_1_0', 0.7071 + 0.0000*I), ('psi_1_1', 0.0000 + 0.0000*I), ('psi_1_2', 0.7071 + 0.0000*I), ('psi_1_3', 0.0000 + 0.0000*I), ('psi_2_0', 0.5000 + 0.0000*I), ('psi_2_1', 0.5000 + 0.0000*I), ('psi_2_2', 0.5000 + 0.0000*I), ('psi_2_3', 0.5000 + 0.0000*I), ('psi_3_0', 0.5000 + 0.0000*I), ('psi_3_1', -0.5000 + 0.0000*I), ('psi_3_2', 0.5000 + 0.0000*I), ('psi_3_3', -0.5000 + 0.0000*I), ('psi_4_0', 0.5000 + 0.0000*I), ('psi_4_1', -0.5000 + 0.0000*I), ('psi_4_2', -0.5000 + 0.0000*I), ('psi_4_3', 0.5000 + 0.0000*I), ('psi_5_0', 0.0000 + 0.0000*I), ('psi_5_1', 0.0000 + 0.0000*I), ('psi_5_2', 0.7071 + 0.0000*I), ('psi_5_3', -0.7071 + 0.0000*I), ('psi_6_0', 0.0000 + 0.0000*I), ('psi_6_1', 0.0000 + 0.0000*I), ('psi_6_2', 0.0000 + 0.0000*I), ('psi_6_3', 1.0000 + 0.0000*I), ('q1', (1.0000 + 0.0000j)|0⟩ + (0.0000 + 0.0000j)|1⟩), ('q0', (1.0000 + 0.0000j)|0⟩ + (0.0000 + 0.0000j)|1⟩), ('q0_final', (0.0000 + 0.0000j)|0⟩ + (-0.0000 + -1.0000j)|1⟩), ('q1_final', (0.0000 + 0.0000j)|0⟩ + (-0.0000 + 1.0000j)|1⟩)]), 0.7146570682525635)
Runtime: 0.7187604904174805

Why? Does this tool work properly as usual in this case? Thanks!