From b5202c65c093cd6d34b473cb0dddd4c615207a72 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 16 Jan 2026 23:48:19 +0000
Subject: [PATCH] Initial analysis of segfault issue

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 test_segfault.smt2 | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test_segfault.smt2

diff --git a/test_segfault.smt2 b/test_segfault.smt2
new file mode 100644
index 000000000..1ed811abc
--- /dev/null
+++ b/test_segfault.smt2
@@ -0,0 +1,6 @@
+(declare-const x Bool)
+(declare-const x3 Bool)
+(declare-const x1 Int)
+(declare-fun cd (Int Int) Int)
+(assert (forall ((a Int) (b Int) (c Int)) (or (<= a 1) (<= b 1) (exists ((d Int)) (and (ite (ite (<= (to_int (+ 1.0 0.00000001 (* (to_real b) (to_real b) (to_real b)))) (cd 0 0)) true (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* (to_real b) (to_real b) (to_real b))))) (is_int (/ 0.00000001 (+ 1.0 (to_real d)))) (ite (< (abs (to_real b)) 0.00000001) true (ite (<= (abs b) (cd 0 c)) (is_int (/ (+ 0.00000001 (* (to_real x1) (to_real x1) (to_real (to_int (/ 1.0 (to_real b)))))) (+ 1 1.0))) x3))) (ite (ite (<= b (cd 0 0)) (is_int (+ 1.0 (* (/ 1.0 1000000000.0)) (* (to_real a) (to_real a) (to_real a)))) (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* 0.00000001 (to_real x1) (to_real a)) (* (to_real a) (to_real a) (to_real a))))) x (ite (< a 1.0) true (ite (<= b (cd 0 0)) true (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* (to_real (to_int (/ (to_real d) (+ 1.0 1.0)))) (to_real (to_int (/ (to_real x1) (+ 1.0 (to_real a))))) (to_real (to_int (/ (to_real x1) (+ 1.0 (to_real a))))))))))))))))
+(check-sat)