mirror of
https://github.com/Z3Prover/z3
synced 2026-06-19 15:16:29 +00:00
Merge pull request #2 from davedets/fix-errors2
Fixes necessary to compile z3 included in clang-tidy via FetchContents.
This commit is contained in:
commit
d2a782fb68
4 changed files with 6 additions and 6 deletions
|
|
@ -66,7 +66,7 @@ z3_add_component(api
|
|||
z3_replayer.cpp
|
||||
${full_path_generated_files}
|
||||
COMPONENT_DEPENDENCIES
|
||||
opt
|
||||
z3_opt
|
||||
euf
|
||||
portfolio
|
||||
realclosure
|
||||
|
|
|
|||
|
|
@ -4925,7 +4925,7 @@ namespace z3 {
|
|||
|
||||
void check_context(rcf_num const& other) const {
|
||||
if (m_ctx != other.m_ctx) {
|
||||
throw exception("rcf_num objects from different contexts");
|
||||
Z3_THROW(exception("rcf_num objects from different contexts"));
|
||||
}
|
||||
}
|
||||
|
||||
|
|
@ -5105,9 +5105,9 @@ namespace z3 {
|
|||
*/
|
||||
inline std::vector<rcf_num> rcf_roots(context& c, std::vector<rcf_num> const& coeffs) {
|
||||
if (coeffs.empty()) {
|
||||
throw exception("polynomial coefficients cannot be empty");
|
||||
Z3_THROW(exception("polynomial coefficients cannot be empty"));
|
||||
}
|
||||
|
||||
|
||||
unsigned n = static_cast<unsigned>(coeffs.size());
|
||||
std::vector<Z3_rcf_num> a(n);
|
||||
std::vector<Z3_rcf_num> roots(n);
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
z3_add_component(opt
|
||||
z3_add_component(z3_opt
|
||||
SOURCES
|
||||
maxcore.cpp
|
||||
maxlex.cpp
|
||||
|
|
|
|||
|
|
@ -8,7 +8,7 @@ set (shell_object_files "")
|
|||
|
||||
# We are only using these dependencies to enforce a build
|
||||
# order. We don't use this list for actual linking.
|
||||
set(shell_deps api extra_cmds opt sat)
|
||||
set(shell_deps api extra_cmds z3_opt sat)
|
||||
z3_expand_dependencies(shell_expanded_deps ${shell_deps})
|
||||
get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS)
|
||||
foreach (component ${Z3_LIBZ3_COMPONENTS_LIST})
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue