diff --git a/Src/COLIBRI/colDomain.pl b/Src/COLIBRI/colDomain.pl
index 83051e862232278fb32baea7e496f3302f317e14..4eebad3f7c97f29d465e31e1b54afde6b44f2dea 100755
--- a/Src/COLIBRI/colDomain.pl
+++ b/Src/COLIBRI/colDomain.pl
@@ -356,6 +356,7 @@ type_from_nonvar(T,Type):-
->
Type = bool
; ((call(lustre_enum(L))@eclipse, % defini dans le fichier .prog
+ atomic(T),
occurs(T,L))
->
Type = enum(L)
diff --git a/Src/COLIBRI/col_solve.pl b/Src/COLIBRI/col_solve.pl
index 5907bf428e3b6748dc3d6adc13b63168f41a839e..a0ee7c7cd8055303339dafd9e1322275eb23a9d4 100644
--- a/Src/COLIBRI/col_solve.pl
+++ b/Src/COLIBRI/col_solve.pl
@@ -680,11 +680,11 @@ smt_test(TO,Size) :-
%StrDir = "./colibri-master-tests/tests/",
%StrDir = "./colibri-master-tests/tests/sat/",
%StrDir = "./colibri-master-tests/tests/unsat/",
- StrDir = "./colibri-master-tests/tests/unknown/",
+ %StrDir = "./colibri-master-tests/tests/unknown/",
%StrDir = "./smt/",
%StrDir = "./AdaCore/",
- %StrDir = "./AdaCore/smt/",
+ StrDir = "./AdaCore/smt/",
%StrDir = "./QF_LRA/2017-Heizmann-UltimateInvariantSynthesis/",
%StrDir = "./QF_LRA/DTP-Scheduling/",
%StrDir = "./QF_LRA/LassoRanker/",
diff --git a/Src/COLIBRI/ndelta.pl b/Src/COLIBRI/ndelta.pl
index bbe8ce330637a9d2c503344daa087448f0195a27..c9c4176ec44ff8473a6310694a52d6fefe86fb96 100755
--- a/Src/COLIBRI/ndelta.pl
+++ b/Src/COLIBRI/ndelta.pl
@@ -334,6 +334,7 @@ deactivate_check_pu :-
%% sur un graphe conrompu. "pre_unify_delta" permet de traiter
%% le graphe avant que la variable soit instanciee.
%% De plus, on teste l'unifiabilite avant de lancer le traitement du graphe.
+pre_unify_delta(T,T) ?- !.
pre_unify_delta(T1,T2) :-
check_pu(T1,T2),
(is_delta_var(T1) ->
@@ -441,7 +442,9 @@ test_unify_delta_delta(Y, delta(BeforeX,AfterX,Loop,CC), DeltasY) ?-
((match_delta_var(BeforeX,Y,Rel,Cost);
match_delta_var(AfterX,Y,Rel,Cost))
->
- ((Rel,Cost) == (=,0) ->
+ ((Rel == =,
+ Cost =:= 0_1)
+ ->
true
; Rel == '+',
Cost = L..H,
@@ -483,7 +486,7 @@ is_signed_delta_var(X{ndelta:delta(B,A,_Loop,_CC)}) ?-
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% On recupere les deux deltas entre X et Y
%% et C est de la forme B1..B2 pour S = '+'|'#'
-%% (B1 peut etre plus grand que B2)
+%% (B1 peut etre plus grand que B2) ??
get_deltas(X{ndelta:delta(BX,AfterX,(ILX,_),CC1)},Y{ndelta:delta(BY,AfterY,(ILY,_),CC2)},NS,NC) ?-
getval(use_delta,1)@eclipse,
(match_delta_var(AfterX,Y,S,C) ->
@@ -503,17 +506,18 @@ get_deltas(X{ndelta:delta(BX,AfterX,(ILX,_),CC1)},Y{ndelta:delta(BY,AfterY,(ILY,
; true),
% On essaye de reparer le graphe
CC1 = CC2
-/*
- get_priority(Prio),
- set_priority(1),
- check_delta_join(X,Y,_),
- set_priority(Prio)
-*/
; true).
match_delta_var([(Var,R,C)|Deltas],Var,Rel,Cost) ?- !,
Rel = R,
- Cost = C.
+ get_type(Var,Type),
+ (Type == int ->
+ (C = L0..H0 ->
+ L is integer(L0),
+ H is integer(H0),
+ Cost = L..H
+ ; Cost is integer(C))
+ ; Cost = C).
match_delta_var([_|Deltas],Var,Rel,Cost) :-
match_delta_var(Deltas,Var,Rel,Cost).
@@ -801,10 +805,13 @@ clear_deltas_var([(X,S,C)|DL1],Var,DL) :-
(X == Var ->
% On peut echouer
% Pas de '#' ni de '=' (car C <> 0)
- S == '+',
- % C doit accepter 0
- C = L..H,
- L =< 0,H >= 0,
+ (S == '+' ->
+ % C doit accepter 0
+ C = L..H,
+ L =< 0,
+ H >= 0
+ ; S == '=',
+ rational(C) =:= 0_1),
% On ignore ce delta
clear_deltas_var(DL1,Var,DL)
; DL = [(X,S,C)|EndDL],
@@ -1655,10 +1662,26 @@ keep_delta_Previous([(X,S,C)|Before],Y,Loop,Previous,Vars,Last) :-
keep_delta_Previous(Before,Y,Loop,NPrevious,NVars,Last)
; keep_delta_Previous(Before,Y,Loop,Previous,Vars,Last)).
-get_delta_before_after(V{ndelta:delta(B,A,_,_CC)},Before,After) ?-
+get_delta_before_after(V{ndelta:delta(B0,A0,_,_CC)},Before,After) ?-
getval(use_delta,1)@eclipse,!,
- Before = B,
- After = A.
+ get_type(V,Type),
+ (Type == int ->
+ (foreach((B,SB,CB0),B0),
+ foreach((B,SB,CB),Before) do
+ (CB0 = LB0..HB0 ->
+ integer(LB0,LB),
+ integer(HB0,HB),
+ CB = LB..HB
+ ; integer(CB0,CB))),
+ (foreach((A,SA,CA0),A0),
+ foreach((A,SA,CA),After) do
+ (CA0 = LA0..HA0 ->
+ integer(LA0,LA),
+ integer(HA0,HA),
+ CA = LA..HA
+ ; integer(CA0,CA)))
+ ; Before = B0,
+ After = A0).
get_delta_before_after(_,[],[]).
diff --git a/test.sh b/test.sh
index c5df76ac5608978b3f951f9b4728857fcb43fccc..04d5edab032a7ad84f01e0939e62d5e731d44a16 100755
--- a/test.sh
+++ b/test.sh
@@ -1,4 +1,4 @@
-#!/bin/sh -u
+#!/bin/sh -eu
STEPS=100
diff --git a/tests/sat/bug_26.smt2 b/tests/sat/bug_26.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..f6c5e1821725ee891cce1f8b3c40b09320586591
--- /dev/null
+++ b/tests/sat/bug_26.smt2
@@ -0,0 +1,20 @@
+;; produced by colibri.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+(define-fun in_range ((x Int)) Bool (and (<= (- 2147483648) x) (<= x 2147483647)))
+
+(declare-const salt (_ BitVec 64))
+
+(declare-const hash (_ BitVec 64))
+
+(define-fun o () Int (bv2nat (bvxor (bvmul #x0000000000000005 salt) (bvmul #x0000000000000007 hash))))
+
+;; Ensures
+ (assert (in_range o))
+
+(assert
+;; defqtvc
+ ;; File "usergroup_examples.adb", line 42, characters 0-0
+ (not (<= 1 (mod o 256))))
+(check-sat)
diff --git a/tests/sat/bug_26_bv.smt2 b/tests/sat/bug_26_bv.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..22bc10da3fc2529378b21ab1b66cf617df521659
--- /dev/null
+++ b/tests/sat/bug_26_bv.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(declare-const salt (_ BitVec 64))
+(declare-const hash (_ BitVec 64))
+(define-fun o () (_ BitVec 64) (bvxor (bvmul #x0000000000000005 salt) (bvmul #x0000000000000007 hash)))
+(assert
+;; defqtvc
+ ;; File "usergroup_examples.adb", line 42, characters 0-0
+ (not (bvult #x0000000000000000 (bvurem o #x0000000000000100))))
+(check-sat)