ASSERTION VIOLATION, File: ../src/qe/qe_mbp.cpp, Line: 572

[merlinsun]

Hi,
For this instance, z3 4d9af78 debug build

$ z3 small.smt2          
ASSERTION VIOLATION
File: ../src/qe/qe_mbp.cpp
Line: 572
!eval.is_false(fml)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
$ cat small.smt2
(declare-fun a () (Array (Array Bool Bool) Bool))
(declare-fun va () (Array (Array (Array Bool Bool) Bool) (Array (Array Bool Bool) Bool)))
(declare-fun r () (Array Bool Bool))
(declare-fun r1 () (Array (Array Bool Bool) Bool))
(assert (forall ((v (Array Int (Array (Array Bool Bool) Bool)))) (distinct a r1 (v 0) (select (store va a (store (v 0) r false)) a))))
(check-sat-using qsat)

[NikolajBjorner]

@hgvk94 - it appears to be within qel_project and how it handles distinct.
The model evaluates (not (distrinct ....)) of several arguments to false. However, two of the arrays are constant false under the model.

(let ((a!1 (distinct ((as const (Array (Array Bool Bool) Bool)) true)
                     ((as const (Array (Array Bool Bool) Bool)) false)
                     (store ((as const (Array (Array Bool Bool) Bool)) false)
                            (store ((as const (Array Bool Bool)) false)
                                   false
                                   true)
                            true)
                     (store ((as const (Array (Array Bool Bool) Bool)) false)
                            (store ((as const (Array Bool Bool)) false)
                                   false
                                   true)
                            false))))
  (not a!1))

[hgvk94]

Yes, we just dodn't support distinct in the new MBP. I am working on fixing this.

[hgvk94]

I have fixed this (and the duplicate issue #6913) locally. Will submit a PR in the next couple of days.

[NikolajBjorner]

would be good as I am planning to drop an updated release in the next couple of days as well.