projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d4b2f06) | patch
Do not check FP at last call if not necessary (#5627)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Dec 2020 01:59:51 +0000 (19:59 -0600)
committerGitHub <noreply@github.com>
Wed, 9 Dec 2020 01:59:51 +0000 (19:59 -0600)
commit6444abbbcf5f298045c32ce3d69033b8f93a41d8
tree225299c73758c80330f63e2300c1e1207a0c4ed2tree
parentd4b2f061182734c8c8efdea38e7afeaca7122fadcommit | diff
Do not check FP at last call if not necessary (#5627)

This makes the theory of floating points not request a last call effort check, if that call is known to do nothing.

This should make CVC4 (more) agnostic to whether --symfpu is enabled during configuration.
src/theory/fp/theory_fp.cpp diff | blob | history
src/theory/fp/theory_fp.h diff | blob | history