mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
0e3fc3687f
* Exporing rounding mode to SMT * Adding round as a non indexed primitive * Indexed identifier * Poetry * Adding some tests * Reverting Rounding Mode as index * Not relying on input format * Injecting AE type float rounding type into SMT rounding type * Poetry * Style * Poetry * More poetry * Also translating on the native side * Adding missing tests * Rebase artifact * Adding tests and some poetry
8 lines
158 B
Plaintext
8 lines
158 B
Plaintext
(set-logic ALL)
|
|
|
|
(set-option :produce-models true)
|
|
(declare-const x Real)
|
|
(assert (> x 0.0))
|
|
(assert (= ((_ ae.round 1 2) RTZ 0.3) x))
|
|
(check-sat)
|
|
(get-model) |