From: mudathirmahgoub <mudathirmahgoub@gmail.com>
Date: Wed, 2 Feb 2022 14:16:26 +0000 (-0600)
Subject: Fix parser issue with tuple_project operator (#8021)
X-Git-Tag: cvc5-1.0.0~482
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f5f14bdd28eeed3a66b0c627968402e5ac2c68db;p=cvc5.git

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)
---

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<api::Term>& 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;
   }