diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-29 20:45:37 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-29 20:45:37 -0500 |
| commit | 9c4a895589fb2da18fd5e178394601ef62b0563f (patch) | |
| tree | 764fcdea9afd47283da37581a0a9e5ba8180b7ba /src/theory/arith/nonlinear_extension.h | |
| parent | 6cdf6fb87a48c04b72722382f43b7fded0b97778 (diff) | |
Improvements to simple transcendental function check model. (#1823)
Diffstat (limited to 'src/theory/arith/nonlinear_extension.h')
| -rw-r--r-- | src/theory/arith/nonlinear_extension.h | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h index c7e6b2b2a..6985f69dd 100644 --- a/src/theory/arith/nonlinear_extension.h +++ b/src/theory/arith/nonlinear_extension.h @@ -281,6 +281,7 @@ class NonlinearExtension { * 2.0*sin( 1 ) > 1.5 * -1.0*sin( 1 ) < -0.79 * -1.0*sin( 1 ) > -0.91 + * sin( 1 )*sin( 1 ) + sin( 1 ) > 0.0 * It will return false for literals like: * sin( 1 ) > 0.85 * It will also return false for literals like: |