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

Add regression tests for issue 43

parent 3b767388
No related branches found
No related tags found
1 merge request!24Fixes #43
Pipeline #37708 failed
(set-logic ALL)
(set-info :smt-lib-version 2.6)
(define-fun in_range1 ((x Int)) Bool (and (<= (- 2147483648) x) (<= x 2147483647)))
(declare-const x Int)
(define-fun res () Int (- x (colibri_cdiv (- (* 2 x) 1) 2)))
;; Ensures
(assert (in_range1 res))
;; H
(assert (<= 0 x))
(assert
;; defqtvc
;; File "arithmetic.adb", line 291, characters 0-0
(not (= res 0)))
(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