From c3db484f1935eb7c64c13bfbdd82cacceca45df0 Mon Sep 17 00:00:00 2001
From: ChrisRackauckas-Claude <accounts@chrisrackauckas.com>
Date: Thu, 20 Aug 2026 06:41:22 -0400
Subject: [PATCH] Add PrecompileTools workload for SymbolicSMT

Co-Authored-By: Chris Rackauckas <accounts@chrisrackauckas.com>
---
 Project.toml                |  2 ++
 src/SymbolicSMT.jl          | 12 ++++++++++++
 test/precompile_workload.jl | 10 ++++++++++
 test/runtests.jl            |  3 +++
 4 files changed, 27 insertions(+)
 create mode 100644 test/precompile_workload.jl

diff --git a/Project.toml b/Project.toml
index 9111462..14eb6c2 100644
--- a/Project.toml
+++ b/Project.toml
@@ -4,11 +4,13 @@ authors = ["Shashi Gowda <shashigowda91@gmail.com>"]
 version = "1.4.0"
 
 [deps]
+PrecompileTools = "aea7be01-6a6a-4083-8856-8a6e6704d82a"
 Symbolics = "0c5d862f-8b57-4792-8d23-62f2024744c7"
 SymbolicUtils = "d1185830-fcd6-423d-90d6-eec64667417b"
 Z3 = "06b161dc-0161-11ea-0f74-41f836f4024b"
 
 [compat]
+PrecompileTools = "1.2"
 Symbolics = "7"
 SymbolicUtils = "4.3"
 Z3 = "1.0"
diff --git a/src/SymbolicSMT.jl b/src/SymbolicSMT.jl
index e6a07f9..8eacb07 100644
--- a/src/SymbolicSMT.jl
+++ b/src/SymbolicSMT.jl
@@ -6,6 +6,7 @@ import Symbolics
 using Symbolics: Num, unwrap, wrap, @variables
 import Z3
 using Z3: BoolVal, BoolVar, Context, Float64Val, IntVal, IntVar, Solver, add, check
+using PrecompileTools: @compile_workload, @setup_workload
 
 export Constraints, issatisfiable, isprovable, resolve, unsat_core
 # Re-export useful Symbolics.jl functionality
@@ -555,4 +556,15 @@ function resolve(expr::Num, cs::Constraints)
     return result isa Bool ? result : wrap(result)
 end
 
+@setup_workload begin
+    @variables x::Real
+    constraints = Constraints([x > 0])
+
+    @compile_workload begin
+        issatisfiable(x > 1, constraints)
+        isprovable(x > 0, constraints)
+        resolve(x > 1, constraints)
+    end
+end
+
 end # module
diff --git a/test/precompile_workload.jl b/test/precompile_workload.jl
new file mode 100644
index 0000000..1ce6213
--- /dev/null
+++ b/test/precompile_workload.jl
@@ -0,0 +1,10 @@
+using SymbolicSMT
+using Symbolics
+using Test
+
+@variables x::Real
+constraints = Constraints([x > 0])
+
+@test issatisfiable(x > 1, constraints)
+@test isprovable(x > 0, constraints)
+@test isequal(resolve(x > 1, constraints), x > 1)
diff --git a/test/runtests.jl b/test/runtests.jl
index 757c152..fd474a9 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -23,6 +23,9 @@ if GROUP == "All" || GROUP == "Core"
         @safetestset "Regression Tests" begin
             include("regression.jl")
         end
+        @safetestset "Precompile workload" begin
+            include("precompile_workload.jl")
+        end
         @safetestset "Unsat Core Tests" begin
             include("unsat_core.jl")
         end