Timeout not working on z3 python in the second `s.check()` call

I have the following python program:

from z3 import *
x = Real('x')
y = Real('y')
a = Real('a')
b = Real('b')
r = Real('r')

s = Solver()
s.set("timeout",600)

f1 = And(0 > 0 + 1*x*x*a*a + 1*y*y*b*b + -1*a*a*b*b,\
        0 + 1*x*x + 1*y*y + -20*x + -20*y + -1*r*r + 200 < 0)
s.add(f1)
s.check()

f_name = "some_constraints.smt"
with open(f_name, 'r') as file:
    smt_content = file.read()
m2 = z3.parse_smt2_string(smt_content)[0]

s.set("timeout",600)
s.add(Not(m2))
s.set("timeout",600)

print(s.check())

In the program if I comment out the first s.check() call the program behaves as expected. That is, it terminates with the output as unknown, whereas the program in its current form doesn't terminate for some reason.

The contents of some_constraints.smt file are as follows:

; 
(set-info :status unknown)
(declare-fun r () Real)
(declare-fun a () Real)
(declare-fun b () Real)
(assert
 (let ((?x22 (* 2.0 r)))
 (let ((?x28 (+ ?x22 19.0)))
 (let (($x107 (< ?x28 0.0)))
 (let ((?x33 (* (* 1.0 a) a)))
 (let ((?x99 (* 400.0 ?x33)))
 (let ((?x100 (* (- 1.0) ?x99)))
 (let ((?x102 (+ (* (- 1.0) (* (* 1.0 b) b)) ?x100)))
 (let ((?x44 (* (* 1.0 b) b)))
 (let ((?x64 (* ?x33 ?x44)))
 (let ((?x86 (* 4.0 ?x64)))
 (let ((?x103 (+ ?x86 ?x102)))
 (let (($x104 (> ?x103 0.0)))
 (let (($x108 (and $x104 $x107)))
 (let ((?x24 (* (- 1.0) 19.0)))
 (let ((?x25 (+ ?x22 ?x24)))
 (let (($x105 (> ?x25 0.0)))
 (let (($x106 (and $x104 $x105)))
 (let (($x109 (or $x106 $x108)))
 (let ((?x88 (* 761.0 ?x33)))
 (let ((?x89 (* (- 1.0) ?x88)))
 (let ((?x90 (+ ?x44 ?x89)))
 (let ((?x92 (+ (* (- 1.0) ?x86) ?x90)))
 (let ((?x37 (* (* 1.0 r) r)))
 (let ((?x84 (* ?x33 ?x37)))
 (let ((?x85 (* 4.0 ?x84)))
 (let ((?x93 (+ ?x85 ?x92)))
 (let (($x94 (> ?x93 0.0)))
 (let ((?x7 (* 2.0 a)))
 (let ((?x15 (+ ?x7 1.0)))
 (let (($x96 (< ?x15 0.0)))
 (let (($x97 (and $x96 $x94)))
 (let (($x110 (or $x97 $x109)))
 (let ((?x10 (* (- 1.0) 1.0)))
 (let ((?x11 (+ ?x7 ?x10)))
 (let (($x82 (> ?x11 0.0)))
 (let (($x95 (and $x82 $x94)))
 (let (($x111 (or $x95 $x110)))
 (let ((?x35 (* (* ?x33 a) a)))
 (let ((?x67 (* 579121.0 ?x35)))
 (let ((?x65 (* 78.0 ?x64)))
 (let ((?x68 (+ ?x65 ?x67)))
 (let ((?x70 (+ (* (- 1.0) (* 312.0 (* ?x35 ?x44))) ?x68)))
 (let ((?x55 (* (* ?x44 b) b)))
 (let ((?x71 (+ ?x55 ?x70)))
 (let ((?x73 (+ (* (- 1.0) (* 8.0 (* ?x33 ?x55))) ?x71)))
 (let ((?x56 (* ?x35 ?x55)))
 (let ((?x57 (* 16.0 ?x56)))
 (let ((?x74 (+ ?x57 ?x73)))
 (let ((?x76 (+ (* (- 1.0) (* 6088.0 (* ?x35 ?x37))) ?x74)))
 (let ((?x45 (* ?x44 ?x37)))
 (let ((?x49 (* ?x33 ?x45)))
 (let ((?x50 (* 8.0 ?x49)))
 (let ((?x77 (+ ?x50 ?x76)))
 (let ((?x79 (+ (* (- 1.0) (* 32.0 (* ?x35 ?x45))) ?x77)))
 (let ((?x39 (* (* ?x37 r) r)))
 (let ((?x40 (* ?x35 ?x39)))
 (let ((?x41 (* 16.0 ?x40)))
 (let ((?x80 (+ ?x41 ?x79)))
 (let (($x81 (< ?x80 0.0)))
 (let (($x112 (or $x81 $x111)))
 (let (($x30 (not (= ?x28 0.0))))
 (let (($x113 (and $x30 $x112)))
 (let (($x27 (not (= ?x25 0.0))))
 (let (($x114 (and $x27 $x113)))
 (let (($x20 (not (= b 0.0))))
 (let (($x115 (and $x20 $x114)))
 (let (($x17 (not (= ?x15 0.0))))
 (let (($x116 (and $x17 $x115)))
 (let (($x14 (not (= ?x11 0.0))))
 (and $x14 $x116)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

Z3Prover / z3

Timeout not working on z3 python in the second `s.check()` call #7234