mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

fixes to mul

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-27 11:58:18 -07:00
parent 4146e938e8
commit ed0ffc1b49
2 changed files with 4 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/sls/bv_sls_eval.cpp
View file

@ -1002,10 +1002,11 @@ namespace bv {
* 8*e = a*(2b), then a = 4e*b^-1
*/
bool sls_eval::try_repair_mul(bvect const& e, bvval& a, bvect const& b) {
verbose_stream() << e << " := " << a << " * " << b << "\n";
unsigned parity_e = a.parity(e);
unsigned parity_b = a.parity(b);
if (a.is_zero(e)) {
if (a.is_zero(b)) {
a.get_variant(m_tmp, m_rand);
if (m_rand(10) != 0)
for (unsigned i = 0; i < b.bw - parity_b; ++i)
@ -1018,6 +1019,8 @@ namespace bv {
return a.set_repair(random_bool(), m_tmp);
}
#if 0
verbose_stream() << "solve for " << e << "\n";