projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b47d656) | patch
Relax an assertion in the evaluator (#8751)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 May 2022 14:58:22 +0000 (09:58 -0500)
committerGitHub <noreply@github.com>
Wed, 11 May 2022 14:58:22 +0000 (07:58 -0700)
commit52b3385489537ba4b5577e1596b74ba0eb0aed21
treeb75f1c535a5562104900f09efc3878d0424d25a0tree
parentb47d65698b514cfbe353182cab8e4261d74a020ecommit | diff
Relax an assertion in the evaluator (#8751)

In a rare case this can throw after https://github.com/cvc5/cvc5/pull/8740, complaining that `(/ 0.0 0)` and `(/ 0.0 0.0)` are not the same.
src/theory/evaluator.cpp diff | blob | history