Conjunction of abstract functions is not able to be asserted

[fosslinux]

It appears that a conjunction of abstract functions is not able to be asserted when it should be.

function f(x: Int): Bool
function g(x: Int): Bool

method foo() {
  assume forall x: Int, y: Int :: {f(x), g(y)} f(x) && g(y)
  assert forall x: Int, y: Int :: {f(x), g(y)} f(x) && g(y)
}

I understand that this should verify. This bug only appears using the Z3 solver; cvc5 passes this.

(also applies to Carbon: see viperproject/carbon#588)

Output:

Silicon found 1 error in 6.18s:
  [0] Assert might fail. Assertion (forall x: Int, y: Int :: { f(x), g(y) } f(x) && g(y)) might not hold. (bug1.vpr@6.10--6.60)

[marcoeilers]

I agree that this is surprising. At first I thought this was somehow related to the way Silicon implements short-circuit semantics for conjunctions, but it actually just seems to be surprising behavior from Z3.

The following SMTLIB code, which is basically what Silicon produces and is what one would expect, results in a double unknown (with both Z3 4.8.7 and 4.16.0):

; ; /z3config.smt2
(set-option :global-decls true) ; Necessary for push pop mode
(set-option :auto_config false)
(set-option :smt.case_split 3)
(set-option :smt.delay_units true)
(set-option :type_check true)
(set-option :smt.mbqi false)
(set-option :pp.bv_literals false)
(set-option :smt.qi.eager_threshold 100)
(set-option :smt.arith.solver 2)
(set-option :model.v2 true)
(set-option :smt.qi.max_multi_patterns 1000)
; 
(push)
(declare-fun f<Bool> (Int) Bool)
(declare-fun g<Bool> (Int) Bool)
(set-option :rlimit 0)

; assume
(assert (forall ((x@1@16 Int) (y@2@16 Int)) (!
  (and (f<Bool> x@1@16) (g<Bool> y@2@16))
  :pattern ((f<Bool> x@1@16) (g<Bool> y@2@16))
  :qid |prog./viper/current/silicon/test.vpr@8@10@8@60|)))

; assert using quantifier
(push) ; 3
(assert (not (forall ((x@9@16 Int) (y@10@16 Int)) (!
  (and (f<Bool> x@9@16) (g<Bool> y@10@16))
  :pattern ((f<Bool> x@9@16) (g<Bool> y@10@16))
  :qid |prog./viper/current/silicon/test.vpr@9@10@9@60|))))
(check-sat)
; unknown
(pop) ; 3

; assert without quantifier
(push) ; 3
(declare-const marcox Int)
(declare-const marcoy Int)
(assert (not
  (and (f<Bool> marcox) (g<Bool> marcoy))
))
(check-sat)
; unknown
(pop) ; 3