Fix sign of sqrt

    since 0 added to sign

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))

src_colibri2/tests/solve/all/sat/test_sqrt_assert_KO_Why3_Colibri2_n_a.psmt2

+;; 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)

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;