diff --git a/src/main/scala/smtlib/lexer/Lexer.scala b/src/main/scala/smtlib/lexer/Lexer.scala index cff5677..f1d4f93 100644 --- a/src/main/scala/smtlib/lexer/Lexer.scala +++ b/src/main/scala/smtlib/lexer/Lexer.scala @@ -11,7 +11,7 @@ class Lexer(reader: java.io.Reader) { import Lexer._ private def isNewLine(c: Char) = c == '\n' || c == '\r' - private def isBlank(c: Char) = c == '\n' || c == '\r' || c == ' ' + private def isBlank(c: Char) = c == '\n' || c == '\r' || c == ' ' || c == '\t' /* * Note that we do not start reading the input until the next function is called. diff --git a/src/test/scala/smtlib/parser/CommandsParserTests.scala b/src/test/scala/smtlib/parser/CommandsParserTests.scala index bffbdc3..90034e9 100644 --- a/src/test/scala/smtlib/parser/CommandsParserTests.scala +++ b/src/test/scala/smtlib/parser/CommandsParserTests.scala @@ -98,6 +98,11 @@ class CommandsParserTests extends AnyFunSuite with TimeLimits { test("Parsing define-fun commands") { + assert(parseUniqueCmd("(define-fun $Perm.isValidVar ((p $Perm)) Bool\n\t(<= $Perm.No p))") === + DefineFun(FunDef("$Perm.isValidVar", Seq(SortedVar("p", Sort("$Perm"))), Sort("Bool"), FunctionApplication( + QualifiedIdentifier("<="), Seq(QualifiedIdentifier("$Perm.No"), QualifiedIdentifier("p")) + ))) + ) assert(parseUniqueCmd("(define-fun f ((a A)) B a)") === DefineFun(FunDef("f", Seq(SortedVar("a", Sort("A"))), Sort("B"), QualifiedIdentifier("a")))) assert(parseUniqueCmd("(define-fun f ((a A)) B (f a))") ===