diff --git a/azure-pipelines.yml b/azure-pipelines.yml index b3bc0f226..48dcf094a 100644 --- a/azure-pipelines.yml +++ b/azure-pipelines.yml @@ -66,15 +66,6 @@ jobs: scriptPath: scripts/mk_unix_dist.py arguments: --nodotnet --nojava --arch=arm64 pythonInterpreter: $(python) - - task: CopyFiles@2 - inputs: - sourceFolder: dist - contents: '*.zip' - targetFolder: $(Build.ArtifactStagingDirectory) - - task: PublishPipelineArtifact@0 - inputs: - artifactName: 'ManyLinuxBuildArm64' - targetPath: $(Build.ArtifactStagingDirectory) - job: "Ubuntu20OCaml" displayName: "Ubuntu 20 with OCaml" diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index df3dffa61..f369c67c4 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -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";