Z3 Invalid Dumping of Quantified Formulas

[baierd]

CPAchecker found some regressions for Z3 in (more or less) current main here. Essentially, we assume that quantified formulas only contain consts, and not functions. But that is not a issue, except that Z3 does not dump all function declarations, especially the problematic argument #2 in the example of the issues above. Argument #2 is actually (*int@1 (Array (_ BitVec 32) (_ BitVec 32))). Looking at the dump, we see that this is NOT declared:

(declare-fun |main::menor@4| () (_ BitVec 32))
(declare-fun |__ADDRESS_OF_main::array@| () (_ BitVec 32))
(declare-fun *int@2 () (Array (_ BitVec 32) (_ BitVec 32)))
(declare-fun __VERIFIER_nondet_int!3@ () (_ BitVec 32))
(declare-fun |main::SIZE@2| () (_ BitVec 32))
(declare-fun __VERIFIER_nondet_int!2@ () (_ BitVec 32))
(declare-fun |main::__CPAchecker_TMP_0@2| () (_ BitVec 32))
(declare-fun |main::j@4| () (_ BitVec 32))
(assert (exists ((|main::j@3| (_ BitVec 32))
         (|main::menor@3| (_ BitVec 32))
         (*int@1 (Array (_ BitVec 32) (_ BitVec 32))))
  (! (let ((a!1 (not (bvsle (bvadd |__ADDRESS_OF_main::array@|
                                   (bvmul #x00000004
                                          |main::__CPAchecker_TMP_0@2|))
                            #x00000000)))
           (a!2 (= *int@2
                   (store *int@1
                          (bvadd |__ADDRESS_OF_main::array@|
                                 (bvmul #x00000004 |main::j@3|))
                          __VERIFIER_nondet_int!3@)))
           (a!3 (bvsle (select *int@2
                               (bvadd |__ADDRESS_OF_main::array@|
                                      (bvmul #x00000004 |main::j@3|)))
                       |main::menor@3|))
           (a!4 (= |main::menor@4|
                   (select *int@2
                           (bvadd |__ADDRESS_OF_main::array@|
                                  (bvmul #x00000004 |main::j@3|))))))
     (let ((a!5 (and (= |main::SIZE@2| #x00000001)
                     (= |main::__CPAchecker_TMP_0@2| |main::SIZE@2|)
                     (not (bvsle |__ADDRESS_OF_main::array@| #x00000000))
                     (= ((_ extract 1 0) |__ADDRESS_OF_main::array@|) #b00)
                     (not (bvsle (bvadd #x00000004 |__ADDRESS_OF_main::array@|)
                                 #x00000000))
                     a!1
                     (= |main::menor@3| __VERIFIER_nondet_int!2@)
                     (= |main::j@3| #x00000000)
                     (not (bvule |main::SIZE@2| |main::j@3|))
                     a!2
                     a!3
                     a!4))
           (a!6 (and (= |main::SIZE@2| #x00000001)
                     (= |main::__CPAchecker_TMP_0@2| |main::SIZE@2|)
                     (not (bvsle |__ADDRESS_OF_main::array@| #x00000000))
                     (= ((_ extract 1 0) |__ADDRESS_OF_main::array@|) #b00)
                     (not (bvsle (bvadd #x00000004 |__ADDRESS_OF_main::array@|)
                                 #x00000000))
                     a!1
                     (= |main::menor@3| __VERIFIER_nondet_int!2@)
                     (= |main::j@3| #x00000000)
                     (not (bvule |main::SIZE@2| |main::j@3|))
                     a!2
                     (not a!3)
                     (= |main::menor@4| |main::menor@3|))))
       (and (= |main::j@4| (bvadd #x00000001 |main::j@3|)) (or a!5 a!6))))
     :weight 0)))

We should report this, so that all bound variables are added to the decls as well.

Further, you can see the :weight 0 at the end, which is Z3 exclusive, and causes parsing errors for other solvers. We already know that the Z3 devs do not want to remove this, so we should investigate removing this ourselves. (Important: Z3 should still be able to parse the formula afterwards!)

[baierd]

Actually argument #2 is not a function, but really an array.

[baierd]

As a consequence, the substitution is really failing invalidly as well. I'll open a new issue for that.

[daniel-raffler]

Further, you can see the :weight 0 at the end, which is Z3 exclusive, and causes parsing errors for other solvers. We already know that the Z3 devs do not want to remove this, so we should investigate removing this ourselves. (Important: Z3 should still be able to parse the formula afterwards!)

It seems like the weight is not printed if we set it to 1 instead: https://github.com/sosy-lab/java-smt/pull/505/changes/418605f10561c9e81cbb4ce572cdba23e20efd54