Performance regression when using Fixedpoint solver (from 4.13.2 to 4.14.1)
Author: KihongHeoCreated Apr 24, 2025Updated Jul 14, 2026
LabelsHorn
After upgrading from Z3 version 4.13.2 to 4.14.1, I noticed a significant performance regression when using the OCaml bindings to invoke the Fixedpoint (CHC) solver (from <1 sec to >5 hours)
To isolate the issue, I used Fixedpoint.to_string to dump the query into an SMT2 file below. When I run this file using the Z3 command-line tool, the solver responds very quickly. However, when I load and run the same query using the OCaml bindings, the solver becomes noticeably slower.
This behavior did not occur with version 4.13.2, where the performance was consistent between the API and the CLI.
(declare-rel |2:| ((Array Int Int) Bool Int Int Bool Int Int Int Int))
(declare-rel for.body ((Array Int Int) Int Bool Int Int Int))
(declare-rel |1:| ((Array Int Int) Bool Int Int Bool Int Int Int Int))
(declare-rel entry ((Array Int Int)))
(declare-rel for.cond ((Array Int Int) Bool Int Int Int Int Int Int))
(declare-rel |5:| ((Array Int Int) Bool Int Int Bool Bool Int Int Int Int Int))
(declare-rel |7:| ((Array Int Int) Bool Int Int Bool Bool Int Int Int Int Int))
(declare-rel |6:| ((Array Int Int) Bool Int Int Bool Bool Int Int Int Int Int))
(declare-rel |3:| ((Array Int Int) Bool Int Int Bool Int Int Int Int))
(declare-rel for.end ((Array Int Int) Bool Int Int Bool Int Int Int Int))
(declare-rel for.inc ((Array Int Int) Bool Int Bool Int Int Int Int))
(declare-var A (Array Int Int))
(declare-var B Int)
(declare-var C Int)
(declare-var D Int)
(declare-var E Int)
(declare-var F Bool)
(declare-var G Int)
(declare-var H Int)
(declare-var I Bool)
(declare-var J (Array Int Int))
(declare-var K Bool)
(declare-var L Int)
(rule (! (entry A) :named entry!))
(rule (=> (and (= G 5) (= H 0) (entry A) true) (for.cond A F E D C 0 H G)))
(rule (=> (and (= F (< B 5)) (for.cond A I E D C B H G) F) (for.body A E F B H G)))
(rule (=> (and (= F (< B 5)) (for.cond A I E D C B H G) (not F))
(for.end A I E D F C B H G)))
(rule (=> (and (= I (< C G)) (= C (+ H D)) (= D B) (for.body A E F B H G) I)
(|1:| A I E D F C B H G)))
(rule (=> (and (= I (< C G)) (= C (+ H D)) (= D B) (for.body A E F B H G) (not I))
(|2:| A I E D F C B H G)))
(rule (=> (and (|1:| A I E D F C B H G) true) (|3:| A I E D F C B H G)))
(rule (=> (and (= A (store J C B)) (|3:| J I E D F C B H G) true)
(for.inc A I D F C B H G)))
(rule (=> (and (= E (+ B 1)) (for.inc A I D F C B H G) true)
(for.cond A I E D C E H G)))
(rule (=> (and (= F (< B H)) (= B (+ L 10)) (for.end A K G E I D C L H) F)
(|5:| A K G E I F B D C L H)))
(rule (=> (and (= F (< B H)) (= B (+ L 10)) (for.end A K G E I D C L H) (not F))
(|6:| A K G E I F B D C L H)))
(rule (=> (and (|5:| A K G E I F B D C L H) true) (|7:| A K G E I F B D C L H)))
(query |6:|)(query |2:|) ; manually addedSource: Z3Prover/z3