projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 236337b) | patch
Explicitly handle isFinite for rounding modes (#4115)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 19 Mar 2020 04:54:57 +0000 (23:54 -0500)
committerGitHub <noreply@github.com>
Thu, 19 Mar 2020 04:54:57 +0000 (23:54 -0500)
commit1ec2e4637e092f1e62005bb3cffc3696d6099679
treeec30c5ba9b6c6b36df46994f898e37735e360a1etree
parent236337b3df1fa6c7627537f0d783d3d3f568b068commit | diff
Explicitly handle isFinite for rounding modes (#4115)

The function TypeNode::isFinite is designed to compute finiteness without computing cardinality for the sake of efficiency; there was a missing case for rounding modes, leading to an assertion failure.

Fixes #4101.
src/expr/type_node.cpp diff | blob | history