[Consolidated] Bugs in FP logic

[muchang]

For this formula, Z3 gives an invalid model. Feeding the model yields unsat.

[521] % z3release model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
(
 (define-fun c () Float64
  (fp #b0 #b10101000111 #xd42aea2879f2f))
 (define-fun b () Float64
  (fp #b0 #b10101000111 #xd42aea2879f2f))
 (define-fun d () Float64
  (fp #b0 #b00000000000 #xffffffffffdfe))
 (define-fun a () RoundingMode
  roundTowardZero)
)
unsat
[522] % 
[522] % cat small.smt2
(declare-fun a () RoundingMode)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(assert
 (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)
 c (fp.add a c d) b))
(check-sat)
(get-model)
(reset)
(define-fun c () Float64 (fp #b0 #b10101000111 #xd42aea2879f2f))
(define-fun b () Float64 (fp #b0 #b10101000111 #xd42aea2879f2f))
(define-fun d () Float64 (fp #b0 #b00000000000 #xffffffffffdfe))
(define-fun a () RoundingMode roundTowardZero)
(assert
 (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)
 c (fp.add a c d) b))
(check-sat)
[523] %

Commit: 89a6c7a

[NikolajBjorner]

Could you stop filing new FP bugs until old ones are considered?
If you have a stream of invalid model bugs, many are highly likely to be related and duplicates. Do as done elsewhere: just add examples to a main bug.

[muchang]

Okay, Nikolaj. The future FP bugs will go into this thread until the old ones have been addressed.

[rainoftime]

Solution soundness bug
Z3 yields sat, while CVC4 returns unsat.
Z3 gives an invalid model, but the model validator cannot deduce this.

(declare-fun r () (_ FloatingPoint 11 53))
(declare-fun x () (_ FloatingPoint 11 53))
(assert
 (forall ((y (_ FloatingPoint 11 53)) )(let ((?x14 (fp (_ bv1 1) (_ bv1395 11) (_ bv3745288593203359 52))))
 (let (($x53 (= y ?x14)))
 (let (($x17 (= r ?x14)))
 (let (($x56 (not (= (fp.min x y) r))))
 (let (($x10 (= x (fp (_ bv1 1) (_ bv9 11) (_ bv1090604990256491 52)))))
 (let (($x57 (or $x10 $x56 $x17 $x53)))
 (let (($x58 (or $x53 $x17 $x56 $x10)))
 (let (($x59 (or $x53 $x17 $x10 $x56)))
 (let (($x60 (or $x56 $x53 $x10 $x17)))
 (let (($x43 (or $x17)))
 (let (($x65 (or $x53 $x10 $x17 $x56)))
 (let (($x66 (or $x56 $x17 $x53 $x10)))
 (let (($x67 (or $x56)))
 (let (($x70 (or $x10 $x56 $x17))) 
 (and (or $x17 $x53 $x10) (or $x53 $x56 $x17 $x10) $x59 $x65 $x66 $x66 $x67 (or $x17 $x56 $x10 $x53) (or $x10 $x17 $x56) (or $x10 $x56 $x53 $x17) (or $x17 $x53) $x57 $x70 (or $x53 $x56 $x10 $x17) (or $x10 $x56) (or $x56 $x10 $x17 $x53) (or $x10 $x17 $x53 $x56) (or $x56 $x17 $x10) (or $x53 $x10 $x56 $x17) (or $x17 $x10 $x53 $x56) $x70 (or $x17 $x10 $x56 $x53) (or $x17 $x53 $x56 $x10) $x43 $x67 $x66 (or $x10) $x65 $x59 (or $x10 $x53 $x56 $x17) $x59 $x43 (or $x10 $x17 $x56 $x53) $x60 $x58 (or $x56 $x53 $x17 $x10) (or $x17 $x56 $x53) $x60 $x59 $x58 $x57))))))))))))))))
 )
(check-sat)
(get-model)

  (define-fun x () (_ FloatingPoint 11 53)
    (fp #b1 #b00000001001 #x3dfe64308d56b))
  (define-fun r () (_ FloatingPoint 11 53)
    (fp #b1 #b10101110011 #xd4e51f42de09f))

[muchang]

Invalid model bug

[807] % z3release model_validate=true small.smt2
sat
(error "line 6 column 10: an invalid model was generated")
(
  (define-fun c () Float64
    (_ NaN 11 53))
  (define-fun b () Float64
    (fp #b0 #b10001111010 #x0afd96cb39f5a))
  (define-fun d () Float64
    (_ NaN 11 53))
  (define-fun a () RoundingMode
    roundTowardZero)
)
[808] % 
[808] % cat small.smt2
(declare-fun a () RoundingMode)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(assert (= (= d c) (= ((_ to_fp 11 53) a (* 88722839111672996637.0 125000000000000000.0)) b)))
(check-sat)
(get-model)
[809] % 

Commit: 4db41c0

[muchang]

(bit-blast qfaufbv) Segmentfault/Assertion violation at ../src/smt/smt_internalizer.cpp Line: 894

[521] % z3release small.smt2
Segmentation fault
[522] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 894
!b_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[523] % cat small.smt2
(set-option :smt.phase_selection 5)
(set-option :smt.threads 2)
(declare-fun a () RoundingMode)
(declare-fun b () (_ FloatingPoint 5 11))
(assert (fp.leq b ((_ to_fp 5 11) a (_ bv0 2))))
(check-sat-using (then bit-blast qfaufbv))
[524] % 

Commit: 4db41c0

[muchang]

Assertion violation at ../src/util/mpf.cpp Line: 907

[530] % z3release small.smt2
sat
[531] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/util/mpf.cpp
Line: 907
exp(res) < mk_max_exp(x.ebits)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[532] % 
[532] % cat small.smt2
(define-sort FP () (_ FloatingPoint 3 5))
(define-fun a () FP (fp #b0 #b000 #b1111))
(define-fun b () FP (fp #b0 #b110 #b1111))
(define-fun c () FP (fp #b1 #b110 #b1111))
(define-fun d () FP (fp #b0 #b100 #b0000))
(declare-fun e () FP)
(declare-fun f () FP)
(define-fun g ((s FP) (t FP)) Bool
 (and
  (not (fp.isInfinite t))
  (not (fp.isInfinite e))
  (not (fp.isNaN t))
  (fp.isNaN e)
  (= (and (fp.isSubnormal e) (fp.isNormal t))
   (fp.isInfinite (fp.fma RNA s t (ite (= (fp.isZero e) (fp.isPositive t)) c b))))))
(assert (xor (g e f) (exists ((x FP)) (fp.isNormal (fp.fma RNA e f x)))))
(check-sat)
[533] % 

Commit: 4db41c0

[muchang]

Solution soundness bug in FP

[511] % cvc4 -q small.smt2
unsat
[512] % z3release small.smt2
sat
[513] % cat small.smt2
(assert (forall ((a Float32)) (not (fp.isNegative (fp.min a (_ +zero 8 24))))))
(check-sat)
[514] % 

Or

[519] % cvc4 -q small.smt2
unsat
[520] % z3release small.smt2
sat
[521] % 
[521] % cat small.smt2
(declare-const b Float32)
(assert (forall ((d Float32)) (not (fp.isPositive (fp.max b d)))))
(check-sat)
[522] % 

Commit: 4db41c0

[muchang]

Invalid model bug

[527] % z3release model_validate=true small.smt2
sat
(error "line 8 column 10: an invalid model was generated")
(
  (define-fun c () Float64
    (fp #b0 #b10101000111 #xd42aea2879f2f))
  (define-fun b () Float64
    (fp #b0 #b10101000111 #xd42aea2879f2f))
  (define-fun d () Float64
    (fp #b0 #b00000000000 #xffffffffffdfe))
  (define-fun a () RoundingMode
    roundTowardZero)
)
unsat
[528] % cat small.smt2
(declare-fun a () RoundingMode)
(declare-fun b () Float64)
(declare-fun c () Float64)
(declare-fun d () Float64)
(assert
 (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)
  c (fp.add a c d) b))
(check-sat)
(get-model)

(reset)

(define-fun c () Float64 (fp #b0 #b10101000111 #xd42aea2879f2f))
(define-fun b () Float64 (fp #b0 #b10101000111 #xd42aea2879f2f))
(define-fun d () Float64 (fp #b0 #b00000000000 #xffffffffffdfe))
(define-fun a () RoundingMode roundTowardZero)
(assert
 (= ((_ to_fp 11 53) a 1000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000.0)
  c (fp.add a c d) b))
(check-sat)
[529] % 

Commit: 4db41c0

[rainoftime]

(set-option :model_validate true)
(set-option :rewriter.elim_and true)
(set-option :smt.phase_selection 0)
(set-option :smt.threads 2)
(declare-fun fpv0 () Float32)
(declare-fun fpv6 () Float32)
(declare-fun fpv7 () Float32)
(declare-fun v7 () Bool)
(declare-fun v9 () Bool)
(assert (xor v9 v7))
(push)
(check-sat)
(assert (fp.eq (fp.neg fpv0) fpv7 fpv7 ((_ to_fp 8 24) RTP 5.0) (fp.abs (fp.add RTN fpv7 fpv6))))
(check-sat)
(get-model)

z3 delta.out.smt2 
sat
sat
(error "line 14 column 10: an invalid model was generated")
(
  (define-fun v7 () Bool
    true)
  (define-fun fpv7 () Float32
    (_ +zero 8 24))
  (define-fun fpv0 () Float32
    (fp #b1 #x81 #b01000000000000000000000))
  (define-fun fpv6 () Float32
    (_ -zero 8 24))
  (define-fun v9 () Bool
    false)
)

[NikolajBjorner]

@wintersteiger - they seem all or mostly all still open. Disregarding the ones that use threads (can often be reproduced without threads, but some extra tinkering needed), there are both duplicates of other bugs (issue with MBQI and how FP models create interpretations of fp.min/fp.max) and some distinct ones.
I have created https://github.com/Z3Prover/z3test/blob/master/regressions/issues/4889.smt2 to track the repros

[NikolajBjorner]

Commit: 6b0dc6d
OS: Ubuntu 20.04

$ z3 delta.smt2
unsat
$ z3 tactic.default_tactic=smt sat.euf=true delta.smt2
Segmentation fault (core dumped)
$ cat delta.smt2
(assert (forall ((V Float16)) (= ((_ to_fp 5 11) RTN 65535.0 0) (fp (_ bv0 1) (_ bv0 5) (_ bv0 10)))))
(check-sat)

@wintersteiger - there is maybe an assumption that pre-processing simplification avoids the code path that gets hit here. When using default_tactic=smt there is limited pre-processing.
fpa2bv_converter.cpp calls mk_numeral in line 2827 for some expression that isn't a numeral.
The expression is created a few lines above. Looking at fpa_decl_plugin.cpp we see that the mk_numeral method in the plugin does not always create expressions with one parameter. This is the case for NaN and +/- infinity.

[NikolajBjorner]

First of all, I wish you a Merry Christmas!

This is a bug related to (check-sat-using (then sat default)).

OS: ubuntu 20.04
Commit: 6b0dc6d

$ z3 case.smt2
sat
$ z3 case_tactic.smt2 tactic.default_tactic=smt sat.euf=true
unsat
$ z3 case_tactic.smt2
unknown
$ z3 case.smt2 tactic.default_tactic=smt sat.euf=true
unknown
$ z3 case_tactic.smt2 tactic.default_tactic=smt sat.euf=true
unsat
$ cat case.smt2
(declare-fun var4 () (_ FloatingPoint 2 3))
(declare-fun var2 () RoundingMode)
(declare-fun var1 () (_ FloatingPoint 11 53))
(declare-fun var0 () RoundingMode)
(assert (or (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (fp.isZero var4) (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1)))
(check-sat)
$ cat case_tactic.smt2
(declare-fun var4 () (_ FloatingPoint 2 3))
(declare-fun var2 () RoundingMode)
(declare-fun var1 () (_ FloatingPoint 11 53))
(declare-fun var0 () RoundingMode)
(assert (or (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1) (fp.isZero var4) (= var4 (fp.max (_ -zero 2 3) (fp.max (_ +zero 2 3) (_ -zero 2 3)))) (= ((_ to_fp 11 53) var0 (/ 88722839111672996637.0 125000000000000000.0)) var1)))
(check-sat-using (then sat default))

[NikolajBjorner]

Last two bugs imported from #5641

[zhendongsu]

Like #4889 (comment), but simpler:

[516] % z3release small.smt2 
unknown
[517] % z3debug small.smt2 
ASSERTION VIOLATION
File: ../src/util/mpf.cpp
Line: 907
exp(res) < mk_max_exp(x.ebits)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[518] % cat small.smt2 
(define-sort FP () (_ FloatingPoint 3 5))
(assert (exists ((x FP)) (not (fp.isInfinite (fp.fma RNA x x x)))))
(check-sat-using qe_rec)

[zhendongsu]

Similar to #4889 (comment):

[531] % z3release small.smt2
Segmentation fault
[532] % z3debug small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_internalizer.cpp
Line: 901
!b_internalized(n)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[533] % cat small.smt2
(set-option :smt.threads 2)
(declare-fun a () RoundingMode)
(declare-fun b () Float64)
(declare-fun c () Float64)
(assert (= ((_ to_fp 11 53) a 0.0) (fp (_ bv0 1) (_ bv0 11) (_ bv0 52))))
(assert (fp.gt b c))
(check-sat-using qe2)

[wintersteiger]

@nbjorner: these are all either fixed with today's fixes or confirmed duplicates, except:

• Threading issues: I couldn't reproduce the problems with threading, but I didn't try very hard

• Your fpa2bv_converter.cpp calls mk_numeral in line 2827 for some expression that isn't a numeral. doesn't make sense to me, because all of the variables mk_numeral is called on are created just before. They are all MPFs, i.e. all numerals. (NaN and +-Inf are also numerals.) But, I don't see that segfault either, so not sure what's going on there.

• Your sat.euf-related one: I have a simper version that I will pull out into a separate issue

[NikolajBjorner]

Very nice!

• threading - typically it is about incrementality (copying state between solvers) not about threads. These are still fuzz bugs, so user case can be unclear.
• fpa2bv_converter - sounds like I should review
• sat.euf - yes, better to separate these because it is a different code path (except for pre-processing) and bugs can be outside of fp.

[NikolajBjorner]

I went over these and from what I can tell they are either fixed or not reproducing. It is therefore saner to close this issue and then anything left over can be dealt with in other issues.