Skip to content

Commit 5187a24

Browse files
committed
fix grammar for SMT-LIB2 declare-fun
The grammar for the SMT-LIB 2 command declare-fun does not expect a parameter identifier.
1 parent a6a0729 commit 5187a24

File tree

1 file changed

+0
-11
lines changed

1 file changed

+0
-11
lines changed

src/solvers/smt2/smt2_parser.cpp

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -1223,19 +1223,8 @@ typet smt2_parsert::function_signature_declaration()
12231223
mathematical_function_typet::domaint domain;
12241224

12251225
while(smt2_tokenizer.peek() != smt2_tokenizert::CLOSE)
1226-
{
1227-
if(next_token() != smt2_tokenizert::OPEN)
1228-
throw error("expected '(' at beginning of parameter");
1229-
1230-
if(next_token() != smt2_tokenizert::SYMBOL)
1231-
throw error("expected symbol in parameter");
1232-
12331226
domain.push_back(sort());
12341227

1235-
if(next_token() != smt2_tokenizert::CLOSE)
1236-
throw error("expected ')' at end of parameter");
1237-
}
1238-
12391228
next_token(); // eat the ')'
12401229

12411230
typet codomain = sort();

0 commit comments

Comments
 (0)