From ee1cd1a03262ba01e5f04d7db5d58a712abb7279 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 9 Sep 2022 10:28:53 +0200
Subject: [PATCH] Fix sign of sqrt
since 0 added to sign
---
src_colibri2/tests/solve/all/sat/dune.inc | 3 +++
.../all/sat/test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2 | 8 ++++++++
src_colibri2/theories/LRA/dom_product.ml | 3 ++-
3 files changed, 13 insertions(+), 1 deletion(-)
create mode 100644 src_colibri2/tests/solve/all/sat/test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2
diff --git a/src_colibri2/tests/solve/all/sat/dune.inc b/src_colibri2/tests/solve/all/sat/dune.inc
index b36ad2c81..8f0f349d0 100644
--- a/src_colibri2/tests/solve/all/sat/dune.inc
+++ b/src_colibri2/tests/solve/all/sat/dune.inc
@@ -5,5 +5,8 @@
--dont-print-result %{dep:div_abs2.smt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:div_abs2.smt2})) (package colibri2))
(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
+--dont-print-result %{dep:test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat
--dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})) (package colibri2))
(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:union-Union-is_singletonqtvc_2.psmt2})) (package colibri2))
diff --git a/src_colibri2/tests/solve/all/sat/test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2 b/src_colibri2/tests/solve/all/sat/test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2
new file mode 100644
index 000000000..f22237ac6
--- /dev/null
+++ b/src_colibri2/tests/solve/all/sat/test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2
@@ -0,0 +1,8 @@
+;; produced by local colibri2.drv ;;
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+
+;; sqrt_0
+(assert (= (colibri_sqrt 0.0) 0.0))
+
+(check-sat)
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 4ce380cdd..7da8bbdfc 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -335,7 +335,8 @@ let converter d (f : Ground.t) =
(* a = res ^ 2 *)
SolveAbs.assume_equality d a
(Product.of_list A.one [ (res, Q.two) ]);
- SolveSign.assume_equality d res Sign_product.one))
+ (* sign res = sign a (don't forget 0 case) *)
+ SolveSign.assume_equality d res (Sign_product.of_one_node a)))
| { app = { builtin = Expr.Add }; tyargs = []; args; _ } ->
let a, b = IArray.extract2_exn args in
reg a;
--
GitLab