mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-24 14:53:40 +00:00
Code Activity

fix compiler error (2)

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 13:45:22 +01:00
parent 923e4b4bd9
commit c29d04d431
2 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/polysat/viable.cpp
View file

@ -440,7 +440,7 @@ namespace polysat {
template <bool FORWARD> template <bool FORWARD>
bool viable::refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) { bool viable::refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) {
entry* ne = refine_bits(v, val, s.size(v), fbi); entry* ne = refine_bits<FORWARD>(v, val, s.size(v), fbi);
if (!ne) if (!ne)
return true; return true;
intersect(v, ne); intersect(v, ne);

4
src/util/rational.h
View file

@ -670,3 +670,7 @@ inline rational gcd(rational const & r1, rational const & r2, rational & a, rati
rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val); rational::m().gcd(r1.m_val, r2.m_val, a.m_val, b.m_val, result.m_val);
return result; return result;
} }
inline void swap(rational& r1, rational& r2) {
r1.swap(r2);
}