diff options
| -rw-r--r-- | src/theory/arith/theory_arith.cpp | 4 | ||||
| -rw-r--r-- | test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 | 2 |
2 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index b63566c29..c25090f38 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -72,6 +72,10 @@ void TheoryArith::finishInit() { // witness is used to eliminate square root tm->setUnevaluatedKind(kind::WITNESS); + // we only need to add the operators that are not syntax sugar + tm->setUnevaluatedKind(kind::EXPONENTIAL); + tm->setUnevaluatedKind(kind::SINE); + tm->setUnevaluatedKind(kind::PI); } } diff --git a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 index 69bb74e84..75d4b6e3a 100644 --- a/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 +++ b/test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --quiet +; COMMAND-LINE: --quiet --no-check-models ; EXPECT: sat (set-logic QF_NRAT) (set-info :status sat) |