From c5376e9d2aea2b365ec8ee5ad6c2386b5b0108a2 Mon Sep 17 00:00:00 2001
From: Marton Hajdu <mezpusz@hotmail.com>
Date: Thu, 14 May 2026 11:59:21 +0200
Subject: [PATCH] Accept define-const from SMTLIB2.7

---
 Parse/SMTLIB2.cpp | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index 2d8d3d111..5bbc5c249 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -221,6 +221,19 @@ void SMTLIB2::readBenchmark(LExpr* bench)
       continue;
     }
 
+    if (ibRdr.tryAcceptAtom("define-const")) {
+
+      auto name = ibRdr.readAtom();
+      auto oSort = ibRdr.readExpr();
+      auto body = ibRdr.readExpr();
+      LExpr iArgs(LispParser::LIST); // dummy list to avoid passing null below
+      readDefineFun(name,&iArgs,oSort,body,/*recursive=*/false);
+
+      ibRdr.acceptEOL();
+
+      continue;
+    }
+
     bool recursive = false;
     if (ibRdr.tryAcceptAtom("define-fun") || (recursive = ibRdr.tryAcceptAtom("define-fun-rec"))) {