fix property-refresh problem for SMTLIB logic

vprover · May 5, 2024 · f9cebc5 · f9cebc5
1 parent 77916b9
commit f9cebc5
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/Shell/SMTLIBLogic.hpp b/Shell/SMTLIBLogic.hpp
@@ -21,6 +21,9 @@ namespace Shell {
   * (I/R)DL - difference logic - we don't treat specially (fragment of L(I/R)A)
   * UF - uninterpreted function = first order we know and love
   * DT - datatypes (term algebras)
+  *
+  * VERY IMPORTANT if this is changed: must also update SMTLIB2::smtLogicNameStrings
+  * (which themselves must be in alphabetical order, so this is also alphabetic)
   */
 enum SMTLIBLogic {
   SMT_ALIA,
@@ -29,9 +32,9 @@ enum SMTLIBLogic {
   SMT_AUFDTLIA,
   SMT_AUFDTLIRA,
   SMT_AUFDTNIRA,
-  SMT_AUFNIA,
   SMT_AUFLIA,
   SMT_AUFLIRA,
+  SMT_AUFNIA,
   SMT_AUFNIRA,
   SMT_BV,
   SMT_LIA,

diff --git a/Shell/UIHelper.cpp b/Shell/UIHelper.cpp
@@ -380,15 +380,17 @@ Problem* UIHelper::getInputProblem()
 {
   LoadedPiece& topPiece = _loadedPieces.top();
   Problem* res = new Problem(topPiece._units.list());
-
+
+  // NB this must happen immediately, as the Property relies on it
+  res->setSMTLIBLogic(topPiece._smtLibLogic);
+
   if(res->isHigherOrder())
     USER_ERROR(
       "This version of Vampire is not yet HOLy.\n\n"
       "Support for higher-order logic is currently on the ahmed-new-hol branch.\n"
       "HOL should be coming to mainline 'soon'."
     );
 
-  res->setSMTLIBLogic(topPiece._smtLibLogic);
   env.setMainProblem(res);
   return res;
 }