diff --git a/src_colibri2/tests/solve/all/sat/dune.inc b/src_colibri2/tests/solve/all/sat/dune.inc index b36ad2c81748d1665718cdc7dd13459fa99be10d..8f0f349d0f392e98adde6b553eb95e187cfbfe77 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 0000000000000000000000000000000000000000..f22237ac677d4a87f57f0f31084def7044e274b6 --- /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 4ce380cdd07b2e8549111296bc76f1661fd339ef..7da8bbdfc2da0b01e5aa778b15d0a75e26a49284 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;