Merge pull request #651 from vprover/michael-fix-smtlib-numerals

allow defining numerals as non-number sorts in SMT-LIB
vprover · Feb 5, 2025 · 20d8009 · 20d8009
2 parents d2c8969 + 020739b
commit 20d8009
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
@@ -2793,11 +2793,11 @@ SMTLIB2::ParseResult SMTLIB2::parseTermOrFormula(LExpr* body, bool isSort)
           continue;
         }
 
-        if (parseAsSpecConstant(id)) {
+        if (parseAsUserDefinedSymbol(id,exp,false/*isSort*/)) {
           continue;
         }
 
-        if (parseAsUserDefinedSymbol(id,exp,false/*isSort*/)) {
+        if (parseAsSpecConstant(id)) {
           continue;
         }