From e23901fe4d69953da7657a8b95469eedf16f1ad9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 12 Apr 2021 11:40:38 +0200
Subject: [PATCH] Add regression tests for bug 25

---
 tests/sat/mod_repr.smt2 | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 tests/sat/mod_repr.smt2

diff --git a/tests/sat/mod_repr.smt2 b/tests/sat/mod_repr.smt2
new file mode 100644
index 000000000..d25262d03
--- /dev/null
+++ b/tests/sat/mod_repr.smt2
@@ -0,0 +1,18 @@
+;; 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))
-- 
GitLab