-
Notifications
You must be signed in to change notification settings - Fork 36
Open
Description
The value of (A_TEST) is incorrect
`(set-logic QF_NRA)
(define-fun A ((x_1 Real) (y_1 Real) (x_2 Real) (y_2 Real)) Real
(let ((dx (- x_2 x_1))
(dy (- y_2 y_1)))
(+ dx dy)))
(define-fun A_TEST () Real (A 1.0 2.0 3.0 4.0))
(check-sat)
(get-value (A_TEST))
`
result --
delta-sat with delta = 0.001
(
(A_TEST (- 1663200257945600027699299354234472591439890153236653683621073950581730305506979530938669653683971833656634875588834897318676499806856981913194801349600022819607058021044347995860773288183887535089484423645963887866421690699419089346715017757127237419326222929577810158533434413834126455996416))
)
Metadata
Metadata
Assignees
Labels
No labels