diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-22 11:45:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-22 11:45:41 -0500 |
| commit | 0045ba2af7b31243c545828494d11f53e16f59db (patch) | |
| tree | 43a790c1870422901d015d7ce893d872284cd246 /test/regress/regress0 | |
| parent | 4bd54ef0cc862ae8736c97ecca07f80ab31396df (diff) | |
Add trascendental function kinds to list of unevaluated operators (#4640)
Fixes #4636.
This adds transcendental function kinds to the list of unevaluated operators (operators that don't necessarily rewrite to constants when applied to constant children). One consequence of this is that when models are enabled, we cannot solve for equations like (= a (cos b)), since the value of (cos b) is not necessarily evaluable, and hence must be approximated. As a result, we answer the benchmark on #4636 instead of generating an incorrect model (when models are enabled). When models are disabled, we answer "sat". A regression had a similar issue which happened to be succeeding. I've added --no-check-models to this regression (or otherwise we would answer unknown for this benchmark).
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/nl/issue3729-cm-solved-tf.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
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) |