Add div, mod, abs in non-strict parsing mode (#5793)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 21 Jan 2021 18:07:50 +0000 (12:07 -0600)
committerGitHub <noreply@github.com>
Thu, 21 Jan 2021 18:07:50 +0000 (12:07 -0600)
commit98d2ca3ee48cb87e8baa7537c97016cc85ab048d
tree1735a3709837c57d519ed180082fcd38bcb65094
parenta4c67b6e6a777c98aee9b9451f41984f6b5d1072
Add div, mod, abs in non-strict parsing mode (#5793)

The recent change to the parser currently breaks our performance on several critical applications, including the use of CVC4 in Facebook. We should only throw a parse error for div in linear logics when strict mode is enabled.
src/parser/smt2/smt2.cpp
test/regress/regress0/expect/scrub.08.sy
test/regress/regress0/parser/linear_arithmetic_err1.smt2
test/regress/regress0/parser/linear_arithmetic_err2.smt2
test/regress/regress0/parser/linear_arithmetic_err3.smt2