From dc9e18d064815ba8f3fbc4244ee9bdf615b8b148 Mon Sep 17 00:00:00 2001
From: Michael Rawson <michael@rawsons.uk>
Date: Thu, 26 Jun 2025 17:12:56 +0200
Subject: [PATCH] prevent FMB crashes on FOOLish inputs

---
 FMB/FiniteModelMultiSorted.cpp | 10 ++--------
 FMB/SortInference.cpp          |  2 ++
 Kernel/Signature.hpp           |  2 ++
 3 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/FMB/FiniteModelMultiSorted.cpp b/FMB/FiniteModelMultiSorted.cpp
index c73b19de5..e831b6b43 100644
--- a/FMB/FiniteModelMultiSorted.cpp
+++ b/FMB/FiniteModelMultiSorted.cpp
@@ -99,8 +99,6 @@ void FiniteModelMultiSorted::initTables()
 
   sortRepr.ensure(env.signature->typeCons());
   for(unsigned s=0;s<env.signature->typeCons();s++){
-    if(env.signature->isInterpretedNonDefault(s))
-      continue;
     sortRepr[s].ensure(_sizes[s]+1);
     for(unsigned i=0;i<=_sizes[s];i++){
       sortRepr[s][i] = -1;
@@ -156,15 +154,11 @@ std::string FiniteModelMultiSorted::toString()
     unsigned size = _sizes[s];
     if(size==0) continue;
 
-    // don't output interpreted sorts at all, we know what they are
-    if(env.signature->isInterpretedNonDefault(s))
-      continue;
-
     std::string sortName = env.signature->typeConName(s);
     std::string sortNameLabel = (env.signature->isBoolCon(s)) ? "bool" : sortName;
 
-    // skip declaring $i, we know what it is
-    if(!env.signature->isDefaultSortCon(s))
+    // skip declaring $i and interpreted sorts, we know what they are
+    if(!env.signature->isDefaultSortCon(s) && !env.signature->isInterpretedNonDefault(s))
       // Sort declaration
       modelStm << "tff(" << prepend("declare_", sortNameLabel) << ",type,"<<sortName<<":$tType)." <<endl;
 
diff --git a/FMB/SortInference.cpp b/FMB/SortInference.cpp
index 01ea35246..f098c7a04 100644
--- a/FMB/SortInference.cpp
+++ b/FMB/SortInference.cpp
@@ -128,6 +128,7 @@ void SortInference::doInference()
           unsigned fresh = env.signature->addFreshFunction(0,"fmbFreshConstant");
           TermList sT = TermList(AtomicSort::createConstant(s));
           env.signature->getFunction(fresh)->setType(OperatorType::getConstantsType(sT));
+          env.signature->getFunction(fresh)->markIntroduced();
           _sig->sortedConstants[dsort].push(fresh);
         }
       }
@@ -498,6 +499,7 @@ void SortInference::doInference()
 #endif
     if(_sig->sortedConstants[s].size()==0 && _sig->sortedFunctions[s].size()>0){
       unsigned fresh = env.signature->addFreshFunction(0,"fmbFreshConstant");
+      env.signature->getFunction(fresh)->markIntroduced();
       _sig->sortedConstants[s].push(fresh);
       freshMap.insert(fresh,s);
       if(firstFreshConstant==UINT_MAX) firstFreshConstant=fresh;
diff --git a/Kernel/Signature.hpp b/Kernel/Signature.hpp
index b18f98112..a701d90f2 100644
--- a/Kernel/Signature.hpp
+++ b/Kernel/Signature.hpp
@@ -836,8 +836,10 @@ class Signature
     if(!_foolConstantsDefined){
       _foolFalse = addFunction("$$false",0); 
       getFunction(_foolFalse)->setType(OperatorType::getConstantsType(AtomicSort::boolSort()));
+      getFunction(_foolFalse)->markIntroduced();
       _foolTrue = addFunction("$$true",0);
       getFunction(_foolTrue)->setType(OperatorType::getConstantsType(AtomicSort::boolSort()));
+      getFunction(_foolTrue)->markIntroduced();
       _foolConstantsDefined=true;
     }
     return isTrue ? _foolTrue : _foolFalse;