From a5048e456333b02d201c3efec2fafe0584f2a5a8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Apr 2025 18:40:06 -0700
Subject: [PATCH] add initial sample agent use case

---
 genaisrc/agentz3.genai.ts | 12 ++++++++++++
 1 file changed, 12 insertions(+)
 create mode 100644 genaisrc/agentz3.genai.ts

diff --git a/genaisrc/agentz3.genai.ts b/genaisrc/agentz3.genai.ts
new file mode 100644
index 000000000..8520d9426
--- /dev/null
+++ b/genaisrc/agentz3.genai.ts
@@ -0,0 +1,12 @@
+script({
+    tools: ["agent_z3"],
+})
+
+$`Solve the following problems using Z3:
+
+Twenty golfers wish to play in foursomes for 5 days. Is it possible for each golfer to play no more
+ than once with any other golfer?
+
+Use SMTLIB2 to formulate the problem as a quantifier free formula over linear integer arithmetic, 
+also known as QF_LIA. The formula should produce an assignemnt to the twenty golfers for the 5 days of foursomes. The SMTLIB2 formula must not contain forall or exists. 
+`
\ No newline at end of file