Fix parser issue with tuple_project operator (#8021)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Wed, 2 Feb 2022 14:16:26 +0000 (08:16 -0600)
committerGitHub <noreply@github.com>
Wed, 2 Feb 2022 14:16:26 +0000 (08:16 -0600)
commitf5f14bdd28eeed3a66b0c627968402e5ac2c68db
tree0536d06906ceaecf46d563b769bc050d5b0e703f
parent2d3c3cd7234488982ad8b769d787a6c69bb9f19e
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