Assertion violation in sat_integrity_checker.cpp:110

[r0ayane]

Hi! For the following instance, z3 with options sat.gc=dyn_psm and sat.gc.initial=100 throws out an assertion violation.

$ cat reduced.smt
(declare-fun a () Int)
(declare-fun b () Int)
(assert (< 1 (* b b a)))
(check-sat)

$ ./z3 reduced.smt 
sat
$ ./z3 reduced.smt sat.gc=dyn_psm sat.gc.initial=100
ASSERTION VIOLATION
File: ../src/sat/sat_integrity_checker.cpp
Line: 110
Failed to verify: num_frozen == s.m_num_frozen

Version: 4.13.4
Commit: 6f24123