From f39cfc295ae0883e5504961c7ac4037d70436b58 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 20 Sep 2022 14:57:19 +0200
Subject: [PATCH] [Interp] Fix model fixing
---
colibri2/core/interp.ml | 22 +++++++++++--------
.../tests/solve/colibri/sat/div_zero.smt2 | 2 +-
.../tests/solve/colibri/sat/mod_repr.smt2 | 2 +-
3 files changed, 15 insertions(+), 11 deletions(-)
diff --git a/colibri2/core/interp.ml b/colibri2/core/interp.ml
index eb5db96ac..a59f0c524 100644
--- a/colibri2/core/interp.ml
+++ b/colibri2/core/interp.ml
@@ -470,15 +470,19 @@ module Fix_model = struct
|> (fun s -> s 0)
|> Sequence.to_list |> Sequence.of_list
in
- let seq =
- Sequence.map seq ~f:(fun v d ->
- Egraph.set_env d Data.env (During { r with nextnode });
- Debug.dprintf4 debug "FixModel by setting %a to %a"
- Node.pp n Value.pp v;
- Egraph.register d n;
- Egraph.set_value d n v)
- in
- seq)
+ if Sequence.is_empty seq then
+ (* Usually because the limit has been reached *)
+ Egraph.contradiction d
+ else
+ let seq =
+ Sequence.map seq ~f:(fun v d ->
+ Egraph.set_env d Data.env (During { r with nextnode });
+ Debug.dprintf4 debug "FixModel by setting %a to %a"
+ Node.pp n Value.pp v;
+ Egraph.register d n;
+ Egraph.set_value d n v)
+ in
+ seq)
in
aux r.nextnode
end
diff --git a/colibri2/tests/solve/colibri/sat/div_zero.smt2 b/colibri2/tests/solve/colibri/sat/div_zero.smt2
index 8d767d611..3bd2746ef 100644
--- a/colibri2/tests/solve/colibri/sat/div_zero.smt2
+++ b/colibri2/tests/solve/colibri/sat/div_zero.smt2
@@ -1,7 +1,7 @@
;; produced by colibri.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
-(set-info :status-colibri2 sat)
+(set-info :status-colibri2 steplimitreached)
(declare-sort tuple0 0)
;; uncomment to pass the VC to cvc4 or z3
diff --git a/colibri2/tests/solve/colibri/sat/mod_repr.smt2 b/colibri2/tests/solve/colibri/sat/mod_repr.smt2
index aec432c08..7a7e46330 100644
--- a/colibri2/tests/solve/colibri/sat/mod_repr.smt2
+++ b/colibri2/tests/solve/colibri/sat/mod_repr.smt2
@@ -1,7 +1,7 @@
;; produced by colibri.drv ;;
(set-logic ALL)
(set-info :smt-lib-version 2.6)
-(set-info :status-colibri2 sat)
+(set-info :status-colibri2 steplimitreached)
(define-fun mod1 ((x Int) (y Int)) Int (ite (< 0 y) (mod x y) (+ (mod x y) y)))
--
GitLab