Add more complicated example on mult

src_colibri2/tests/solve/smt_nra/unsat/dune.inc

@@ -28,3 +28,6 @@
 (rule (alias runtest) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:mul_pos_zero_le.smt2})))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mul_pos_zero_le.smt2})))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:mult_hard.smt2})))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=100M --time=30s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:mult_hard.smt2})))

src_colibri2/tests/solve/smt_nra/unsat/mult_hard.smt2

+(set-logic ALL)
+
+(declare-const x Real)
+(declare-const y Real)
+(declare-const v Real)
+(declare-const z Real)
+(declare-const w Real)
+
+(assert (< 0 x))
+(assert (< 0 y))
+(assert (< 0 v))
+(assert (< 0 z))
+(assert (< 0 w))
+
+;(assert (not (= y 0.0)))
+;(assert (not (= v 0.0)))
+;(assert (< 0.0 (* z w)))
+
+(assert (= (* x y) (/ z (* y (* v v)))))
+(assert (= (* (* y v) (* y v)) (/ z w)))
+(assert (not (= w x)))
+(check-sat)
+
+; &xy=zy^{-1}v^{-2} & yv = \sqrt{\frac{z}{w}} \\