1 files changed, 8 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index b99e142ba..fc930dc79 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -295,7 +295,8 @@ public:
       case kind::BITVECTOR_MULT:
       case kind::BITVECTOR_PLUS:
         if(numArgs != 2) {
-          parseError("Operator requires exact 2 arguments in strict SMT-LIB compliance mode: " + kindToString(kind));
+          parseError("Operator requires exact 2 arguments in strict SMT-LIB "
+                     "compliance mode: " + kindToString(kind));
         }
         break;
       default:
@@ -304,6 +305,12 @@ public:
     }
   }
 
+  // Throw a ParserException with msg appended with the current logic.
+  inline void parseErrorLogic(const std::string& msg) throw(ParserException) {
+    const std::string withLogic = msg + getLogic().getLogicString();
+    parseError(withLogic);
+  }
+
 private:
   std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type;
   std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars;