projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d758a32) | patch
Use theoryof-mode=type for QF_NRA (#5326)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 22 Oct 2020 18:06:51 +0000 (20:06 +0200)
committerGitHub <noreply@github.com>
Thu, 22 Oct 2020 18:06:51 +0000 (20:06 +0200)
commita7aba0c8580d5153fee99b4d59345e33c39c893b
treebca5ab1672ed411119d53273c5e8c4d571142eeatree
parentd758a32f5bb1361d766a71c3d2cdaeacb8f39a76commit | diff
Use theoryof-mode=type for QF_NRA (#5326)

We've observed that our QF_NRA solving benefits significantly from --theoryof-mode=type across the board (of other options that influence QF_NRA solving). This PR sets type as the new default for QF_NRA solving.
src/smt/set_defaults.cpp diff | blob | history