Make isBuiltinFunction return true for frameTerms

src/api/MainSolver.cc

@@ -9,6 +9,7 @@
 #include "MainSolver.h"
 
 #include <common/ApiException.h>
+#include <common/NonLinException.h>
 #include <itehandler/IteHandler.h>
 #include <logics/ArrayTheory.h>
 #include <logics/LATheory.h>
@@ -333,14 +334,23 @@ sstat MainSolver::check() {
         StopWatch sw(query_timer);
     }
     if (isLastFrameUnsat()) { return s_False; }
-    sstat rval = simplifyFormulas();
+    sstat rval;
+    try {
+        rval = simplifyFormulas();
+    } catch (NonLinException const & error) {
+        reasonUnknown = error.what();
+        return s_Undef;
+    }
 
     if (config.dump_query()) printCurrentAssertionsAsQuery();
 
     if (rval == s_Undef) {
         try {
             rval = solve();
-        } catch (std::overflow_error const & error) { rval = s_Error; }
+        } catch (std::overflow_error const & error) { rval = s_Error; } catch (NonLinException const & error) {
+            reasonUnknown = error.what();
+            return s_Undef;
+        }
         if (rval == s_False) {
             assert(not smt_solver->isOK());
             rememberUnsatFrame(smt_solver->getConflictFrame());

src/api/MainSolver.h

@@ -258,7 +258,7 @@ class MainSolver {
     PTRef newFrameTerm(FrameId frameId) {
         assert(frameId != 0);
         auto name = std::string(Logic::s_framev_prefix) + std::to_string(frameId);
-        PTRef frameTerm = logic.mkBoolVar(name.c_str());
+        PTRef frameTerm = logic.mkInternalBoolVar(name.c_str());
         Lit l = term_mapper->getOrCreateLit(frameTerm);
         term_mapper->setFrozen(var(l));
         smt_solver->addAssumptionVar(var(l));
@@ -310,6 +310,7 @@ class MainSolver {
     vec<PTRef> frameTerms;
     std::size_t firstNotSimplifiedFrame = 0;
     unsigned int insertedFormulasCount = 0;
+    std::string reasonUnknown;
 };
 
 bool MainSolver::trackPartitions() const {

src/common/CMakeLists.txt

@@ -24,5 +24,5 @@ include(numbers/CMakeLists.txt)
 install(FILES
         StringMap.h Timer.h inttypes.h IColor.h
         TreeOps.h FlaPartitionMap.h PartitionInfo.h Partitions.h ApiException.h TypeUtils.h
-        NatSet.h ScopedVector.h TermNames.h
+        NatSet.h ScopedVector.h TermNames.h NonLinException.h
 DESTINATION ${INSTALL_HEADERS_DIR}/common)

src/common/NonLinException.h

@@ -0,0 +1,19 @@
+/*
+*  Copyright (c) 2024, Konstantin Britikov <britikovki@gmail.com>
+*
+*  SPDX-License-Identifier: MIT
+*/
+
+#ifndef OPENSMT_NONLINEXCEPTION_H
+#define OPENSMT_NONLINEXCEPTION_H
+
+#include <stdexcept>
+
+namespace opensmt {
+class NonLinException : public std::runtime_error {
+public:
+    NonLinException(std::string_view const reason_) : runtime_error("Term " + std::string(reason_) + " is non-linear"){}
+};
+}
+
+#endif // OPENSMT_NONLINEXCEPTION_H