opsem/calloc.01.ll sat with z3-4.8.9 but unknown with z3-4.11.2

[priyasiddharth]

Exact same command line and generated smt2 file

"/home/siddharth/seahorn/seahorn-12/seahorn/build-dbg/run/bin/seahorn" "--horn-bmc-engine=mono" "--horn-bmc" "--horn-shadow-mem-alloc-is-def" "--horn-bv2=true" "--log=opsem" "--keep-shadows=true" "--horn-solve" "--horn-bv2-lambdas" "--log=opsem3" "/home/siddharth/seahorn/seahorn-12/seahorn/test/opsem/calloc.01.ll" --o=calloc.smt2

z3 4.8.9

siddharth@pop-os ~/seahorn/seahorn-12/seahorn (dev14) $ cat calloc-z3_4.8.9.smt2 |sprunge

http://sprunge.us/Smstdl

z3 4.11.2

siddharth@pop-os ~/seahorn/seahorn-12/seahorn (dev14) $ cat calloc-z3_4.11.2.smt2 |sprunge

http://sprunge.us/4GZpQs

[agurfinkel]

is there some issue?

[priyasiddharth]

The test is expected to return sat but with z3-4.11.2 (latest release) it shows unknown after churning for a while. This implies we cannot switch z3 under the hood without hitting this (and maybe more) issues. Is this kind of unstability expected given the smt engine we are hitting?

[agurfinkel]

@priyasiddharth I can confirm that this takes a while with current z3 master. Works quickly with smtfd.
One issue that stands out is that the vc has unexpanded lambda expressions. This is wrong, we do not expect
any lambdas in the VC! This means they are somewhere not beta-reduced.

Not sure why z3 does not beta-reduce them either. So first thing identify why there are lambdas.

This specific line:

(= a!1 (lambda ((addr (_ BitVec 32))) #x00000000))

seems problematic since this is equality over lambda expressions. This is definitely not something we expect.