diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index 3f9b161e01..bd74f7b766 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -1921,37 +1921,19 @@ let fm_simplex_unbounded_integers_encoding env uf =
"case-split over unions of intervals is needed !!!";
assert false
- | [(mn, ex_mn), (mx, ex_mx)] ->
+ | [(lb, ex_lb), (ub, ex_ub)] ->
let l, c = P.to_list p in
- let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in
- assert (Q.sign c = 0);
- let cst0 =
- List.fold_left (fun z (_, c) -> Q.add z (Q.abs c))Q.zero l
- in
- let cst = Q.div cst0 (Q.from_int 2) in
- assert (mn == None || mx == None);
- let min =
- let mn =
- match mn with
- | None -> None
- | Some (q, q') -> Some (Q.add q cst, q')
- in
- bnd_to_simplex_bound (mn, ex_mn)
- in
- let max =
- let mx =
- match mx with
- | None -> None
- | Some (q, q') -> Some (Q.sub q cst, q')
- in
- bnd_to_simplex_bound (mx, ex_mx)
- in
+ assert (Q.is_zero c);
+ assert (lb == None || ub == None);
+ let min = bnd_to_simplex_bound (lb, ex_lb) in
+ let max = bnd_to_simplex_bound (ub, ex_ub) in
match l with
| [] -> assert false
- | [x, c] ->
+ | [c, x] ->
assert (Q.is_one c);
Sim.Assert.var simplex x ?min ?max |> fst
| _ ->
+ let l = List.rev_map (fun (c, x) -> x, c) (List.rev l) in
let xp = alien_of p in
let sim_p =
match Sim.Core.poly_of_slake simplex xp with
@@ -2009,7 +1991,7 @@ let model_from_simplex sim is_int env uf =
)[] (List.rev main_vars)
-let model_from_unbounded_domains =
+let model_from_infinite_domains =
let mk_cs acc (x, v, _ex) =
((LR.view (LR.mk_eq x v)), true,
Th_util.CS (Th_util.Th_arith, Q.from_int 2)) :: acc
@@ -2040,7 +2022,7 @@ let case_split env uf ~for_model =
else
begin
match case_split_union_of_intervals env uf with
- | [] -> model_from_unbounded_domains env uf
+ | [] -> model_from_infinite_domains env uf
| l -> l
end
| _ -> res
diff --git a/tests/dune.inc b/tests/dune.inc
index 26d82ad68c..3224bab3ee 100644
--- a/tests/dune.inc
+++ b/tests/dune.inc
@@ -193838,7 +193838,28 @@
(alias runtest-quick)
(package alt-ergo)
(action
- (diff 340.expected 340_fpa.output))))
+ (diff 340.expected 340_fpa.output)))
+ (rule
+ (target 1022.models_dolmen.output)
+ (deps (:input 1022.models.smt2))
+ (package alt-ergo)
+ (action
+ (chdir %{workspace_root}
+ (with-stdout-to %{target}
+ (ignore-stderr
+ (with-accepted-exit-codes (or 0)
+ (run %{bin:alt-ergo}
+ --timelimit=2
+ --enable-assertions
+ --output=smtlib2
+ --frontend dolmen
+ %{input})))))))
+ (rule
+ (deps 1022.models_dolmen.output)
+ (alias runtest-quick)
+ (package alt-ergo)
+ (action
+ (diff 1022.models.expected 1022.models_dolmen.output))))
; Auto-generated part end
; File auto-generated by gentests
diff --git a/tests/issues/1022.models.expected b/tests/issues/1022.models.expected
new file mode 100644
index 0000000000..c1f647bc74
--- /dev/null
+++ b/tests/issues/1022.models.expected
@@ -0,0 +1,13 @@
+
+unknown
+(
+ (define-fun x () Int 3)
+ (define-fun x1 () Int (- 3))
+ (define-fun x2 () Int (- 2))
+ (define-fun x3 () Int 0)
+ (define-fun x4 () Int (- 1))
+ (define-fun x5 () Int 2)
+ (define-fun x6 () Int 0)
+ (define-fun x7 () Int 0)
+ (define-fun x9 () Int 2)
+)
diff --git a/tests/issues/1022.models.smt2 b/tests/issues/1022.models.smt2
new file mode 100644
index 0000000000..02a8316d1b
--- /dev/null
+++ b/tests/issues/1022.models.smt2
@@ -0,0 +1,24 @@
+(set-option :produce-models true)
+(set-logic QF_LIA)
+(declare-fun x () Int)
+(declare-fun x1 () Int)
+(declare-fun x2 () Int)
+(declare-fun x3 () Int)
+(declare-fun x4 () Int)
+(declare-fun x5 () Int)
+(declare-fun x6 () Int)
+(declare-fun x7 () Int)
+(declare-fun x9 () Int)
+(assert (and
+(< 0 x)
+(< 0 (+ x x2))
+(< 0 (+ x4 x9))
+(< 0 (+ x5 x6))
+(< 0 (* x1 (- 1)))
+(< 1 (+ x3 x5 x9 x2))
+(< 1 (+ x5 (* x3 (- 1))))
+(< 0 (+ x2 (* 27 x7) (* x3 (- 1)) (* x4 (- 26))))
+(< 0 (+ x3 x6 (* 9 x7) (* x1 (- 1)) (* x2 (- 7)) (* x4 (- 14)) (* x5 (- 15))))
+(< (- 39) (+ (* x (- 7)) (* 7 x1) (* 2 x2) (* 18 x4) (* 14 x5) (* x6 (- 3)) (* x7 (- 12)) (* x9 (- 1))))))
+(check-sat)
+(get-model)
diff --git a/tests/issues/777.models.expected b/tests/issues/777.models.expected
index 1a34774938..8d04d7d4b3 100644
--- a/tests/issues/777.models.expected
+++ b/tests/issues/777.models.expected
@@ -1,5 +1,5 @@
unknown
(
- (define-fun i () Int 2)
+ (define-fun i () Int 1)
)
diff --git a/tests/models/uf/uf2.models.expected b/tests/models/uf/uf2.models.expected
index ce06fd3336..902676ae79 100644
--- a/tests/models/uf/uf2.models.expected
+++ b/tests/models/uf/uf2.models.expected
@@ -1,7 +1,7 @@
unknown
(
- (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 2)) 0 2))
+ (define-fun f ((arg_0 Int)) Int (ite (= arg_0 (- 1)) 0 1))
(define-fun a () Int 0)
- (define-fun b () Int (- 2))
+ (define-fun b () Int (- 1))
)