diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-01-21 12:07:50 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-01-21 12:07:50 -0600 |
| commit | 98d2ca3ee48cb87e8baa7537c97016cc85ab048d (patch) | |
| tree | 1735a3709837c57d519ed180082fcd38bcb65094 /src/parser/smt2/smt2.cpp | |
| parent | a4c67b6e6a777c98aee9b9451f41984f6b5d1072 (diff) | |
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.
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
| -rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 0c67299ab..9c5474a47 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -550,7 +550,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) if(d_logic.areIntegersUsed()) { defineType("Int", d_solver->getIntegerSort(), true, true); addArithmeticOperators(); - if (!d_logic.isLinear()) + if (!strictModeEnabled() || !d_logic.isLinear()) { addOperator(api::INTS_DIVISION, "div"); addOperator(api::INTS_MODULUS, "mod"); |