From f5f14bdd28eeed3a66b0c627968402e5ac2c68db Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 2 Feb 2022 08:16:26 -0600 Subject: [PATCH] Fix parser issue with tuple_project operator (#8021) The current parser accepts the smtlib code below since it ignores all arguments after z. This PR fixes this issue by sending all arguments to the operator to be checked. (set-logic ALL) (declare-fun z () (Tuple Int Int Int Int Int Int)) (declare-fun f () (Tuple Int Int Int)) (assert (= f ((_ tuple_project 0 1 2) z f f f f f f f f 0 0 0 0 0))) (check-sat) --- src/parser/smt2/smt2.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index a93596633..62b3d7bf6 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1051,7 +1051,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector& args) } else if (p.d_kind == api::TUPLE_PROJECT) { - api::Term ret = d_solver->mkTerm(p.d_op, args[0]); + api::Term ret = d_solver->mkTerm(p.d_op, args); Debug("parser") << "applyParseOp: return projection " << ret << std::endl; return ret; } -- 2.30.2