summaryrefslogtreecommitdiff
path: root/src/theory/theory_model_builder.cpp
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-10-08 19:44:22 -0700
committerGitHub <noreply@github.com>2018-10-08 19:44:22 -0700
commit0d310d6716d1ab679cd466a2e47e5c0f6cdd8569 (patch)
tree146e3a070038a6d847204c5f4173d9a3bf7b619d /src/theory/theory_model_builder.cpp
parenta1c9b7408ee47ea69ef9866cdac75f839c14bc8d (diff)
BV instantiator: Factor out util functions. (#2604)
Previously, all util functions for the BV instantiator were static functions in theory/quantifiers/cegqi/ceg_bv_instantiator.cpp. For the corresponding unit test, it was therefore required to include this cpp file in order to test these functions. This factors out these functions into a theory/quantifiers/cegqi/ceg_bv_instantiator_utils.(cpp|h). Asan reported errors for the corresponing unit test because of this.
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback