[SMT-LIB] A beginner's question about Wintersteiger's benchmark

[Zhoulai]

Hello,

I am new to SMT-LIB format and want to learn something about the recently
added FP theory. Below is a piece of syntax from the benchmark of
Wintersteiger (thanks): add-has-solution-12196.smt2.


 (set-logic QF_FP)
(set-info :status sat)
(define-sort FPN () (_ FloatingPoint 11 53))
(declare-fun x () FPN)
(declare-fun y () FPN)
(declare-fun r () FPN)
(assert (= x (fp #b0 #b01111101100
#b1110010110001100001110000101110111111011011010000001)))
(assert (= y (fp #b1 #b01010111111
#b1110111010100000001111111010111000001000101111000001)))
(assert (= r (fp #b0 #b01111101100
#b1110010110001100001110000101110111111011011010000000)))
(assert (= (fp.add roundTowardNegative x y) r))
(check-sat)

Question: Am I correct in understanding that the first three 'assert'
specify the values of x,y and r through their sign, exponent, and mantissa,
and the last 'assert' check-sat for x+y==r (with the specified rounding
mode)?

I feel confused since usually we check-sat for a formula where all
variables are *not* yet assigned a concrete value, such as (x+y<=0 /\
x<-y+3).

Thanks.
Zhoulai