[Bug] CNOT gates not working sometimes...

[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.state_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(2)
        times.append(time.time() - start)

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

The execution result of the above code would be:

H(q0), H(q1), H(q2), Z(q2), CNOT(q0, q2), H(q0), H(q1), H(q2)
Concrete execution...

Initial values: [(1, 0), (1, 0), (1, 0)]
Initial state ψ ≐ [[1 0 0 0 0 0 0 0]].T
ψ_0 ≐ [[0.70710678 0.         0.         0.         0.70710678 0.
  0.         0.        ]].T
ψ_1 ≐ [[0.5 0.  0.5 0.  0.5 0.  0.5 0. ]].T
ψ_2 ≐ [[0.35355339 0.35355339 0.35355339 0.35355339 0.35355339 0.35355339
  0.35355339 0.35355339]].T
ψ_3 ≐ [[ 0.35355339 -0.35355339  0.35355339 -0.35355339  0.35355339 -0.35355339
   0.35355339 -0.35355339]].T
ψ_4 ≐ [[ 0.35355339 -0.35355339  0.35355339 -0.35355339  0.35355339 -0.35355339
   0.35355339 -0.35355339]].T
...

We can discover that from ψ_3 to ψ_4, the CNOT(q0, q2) does not swap the pair (vec[4], vec[5]) and the pair (vec[6], vec[7]). Why? Does this tool work properly as usual in this case? Thanks!