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

Add regression tests for bug 25

parent 1ad1ddd8
No related branches found
No related tags found
1 merge request!13Fix bug25
Pipeline #33973 failed
;; produced by colibri.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
(define-fun mod1 ((x Int) (y Int)) Int (ite (< 0 y) (mod x y) (+ (mod x y) y)))
(define-fun in_range1 ((x Int)) Bool (and (<= 1 x) (<= x 100)))
(declare-const x Int)
;; Assume
(assert (in_range1 x))
(assert (not (in_range1 (mod1 (+ x 1) 100))))
(check-sat)
(get-value (x))
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