Parser now throws an Exception when defineFun is used

Author: DavidGalllob

src/org/sosy_lab/java_smt/basicimpl/parserInterpreter/Visitor.java

@@ -56,6 +56,7 @@
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_assertContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_declareConstContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_declareFunContext;
+import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_defineFunContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_defineSortContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_popContext;
 import org.sosy_lab.java_smt.basicimpl.parserInterpreter.Smtlibv2Parser.Cmd_pushContext;
@@ -2300,4 +2301,9 @@ public Object visitResp_get_model(Resp_get_modelContext ctx) {
     isModel = true;
     return visitChildren(ctx);
   }
+
+  @Override
+  public Object visitCmd_defineFun(Cmd_defineFunContext ctx) {
+    throw new UnsupportedOperationException("JavaSMT does not support \"define-fun\"");
+  }
 }