Skip to content
Snippets Groups Projects
Commit cd782201 authored by François Bobot's avatar François Bobot
Browse files

Merge branch 'fix_45' into 'master'

Add regression tests for issue 45

See merge request adacore/colibri!27
parents 3131390d 592f1cea
No related branches found
No related tags found
1 merge request!27Add regression tests for issue 45
Pipeline #42836 failed
;; produced by colibri.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
(declare-const x Float32)
(declare-const y Float32)
(declare-const z Float32)
;; Assume
(assert (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) x))
;; Assume
(assert (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) y))
;; Assume
(assert (fp.leq (fp #b0 #b00000000 #b00000000000000000000000) z))
;; Assume
(assert (fp.leq x (fp #b0 #b10010111 #b00000000000000000000000)))
;; Assume
(assert (fp.leq y (fp #b0 #b10010111 #b00000000000000000000000)))
(assert
(not (= (ite (fp.lt (fp.neg (fp.mul RNE x y)) z) true false) true)))
(check-sat)
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment