smt - z3 returns unknown with unrolled loop for a 16 bitwidth bitvector formula

Question

I'm trying to figure out why the z3 solver returns an unknown for a particular formula.

The formula is representative of a certain piece of code with a loop which does "abstract" multiplication (which is inspired by the long multiplication algorithm).

To check if my abstract algorithm works correctly (passes my verification condition) I encode the negation of the condition to get a counterexample from z3. To encode the formula in z3 understandably involves unrolling the loop. I set the timeout to 0 (i.e. no timeout), and use a SolverFor("QF_BV"). I am using 40 threads with parallel.enable.

While I do get unsat for a bitvector width of 2 through 14, when I choose a bitvector of width 16, z3 gives me an unknown in about 11 hours (this time varies).

Calling .reason_unknown() on the solver, I get: incomplete

Calling .statistics() on the solver gives the following output:

(:eliminated-vars                  1034
 :lh-add-binary                    140371855
 :lh-bca                           23814396
 :lh-bool-var                      2231207637
 :lh-cube-backtracks               105014
 :lh-cube-conflicts                35005
 :lh-cube-cutoffs                  70009
 :lh-double-lookahead-propagations 2528053
 :lh-double-lookahead-rounds       1241284
 :lh-propagations                  158526025
 :lh-windfalls                     26038702
 :max-memory                       44090.71
 :memory                           177.62
 :num-allocs                       27798866265032752.00
 :par-progress                     100.00
 :par-unsat                        34999
 :rlimit-count                     764946247
 :sat-ate                          222268
 :sat-backjumps                    3002301117
 :sat-backtracks                   147
 :sat-bce                          104728
 :sat-conflicts                    3002336240
 :sat-decisions                    3454552584
 :sat-del-clause                   3371028754
 :sat-elim-bool-vars-res           1361521
 :sat-elim-clauses                 1059679366
 :sat-elim-literals                1080799650
 :sat-gc-clause                    1918637627
 :sat-minimized-lits               858977833
 :sat-mk-clause-2ary               40013037
 :sat-mk-clause-3ary               97306887
 :sat-mk-clause-nary               3779658115
 :sat-mk-var                       556299461
 :sat-probing-assigned             122001
 :sat-propagations-2ary            3293681175
 :sat-propagations-3ary            2950499967
 :sat-propagations-nary            3439887739
 :sat-restarts                     371680015
 :sat-scc-elim-binary              3427928
 :sat-scc-elim-vars                1188920
 :sat-subs-resolution              196847601
 :sat-subs-resolution-dyn          1928526157
 :sat-subsumed                     252105065
 :sat-tr                           1131060
 :sat-units                        47282317
 :time                             42930.13)

What is this supposed to mean, and how am I supposed to interpret this? Does z3 return unknown because the solver thinks it will take too long to solve? Or is it because z3 can't even solve it, maybe because the theory isn't expressive enough? Or is it some other reason?

Do let me know if you need any specifics (about the code or the z3 encoding). I also have a run with high verbosity, and can link to a pastebin if needed.

question from:https://stackoverflow.com/questions/66052995/z3-returns-unknown-with-unrolled-loop-for-a-16-bitwidth-bitvector-formula

Answer 1

Waitting for answers