[YICES-HELP] unbounded loop

[Jean-Francois Couchot]

Hi.

I've some difficulties to understand why Yices does not discharge the 
proof obligation joined in attachement in smtlib formalism.

More precisely, the command

$yices -smt -v 10 sstrat.smt

returns
Yices (version 1.0.2). Copyright 2005, 2006 SRI International.
GMP (version 4.1.4). Copyright Free Software Foundation, Inc.
Build date: Mon Nov 13 09:58:33 PST 2006
simplifying...
hash consing...
eliminating term ite...
searching...
ssiIssssiI.s...........s...........s...r.........s.......s
.......s........s.........s.......s......s.......s....r....s
......s...........s............s..........s.............s......s
............s........s......s........s.......s.....................
.........s........s.......s.............s..........s..............s.

Well, it seems that the case spliting rule of the SAT solver is widely 
activated.

However, in the proof obligation, when I comment the two quantified axioms

;; Why axiom ite_true
  :assumption
    (forall (?t_5_200_144 c_type)
    (forall (?x_75_145 c_unique)
    (forall (?y_74_146 c_unique)
    (= (smtlib__ite c_Boolean_true  (c_sort ?t_5_200_144 ?x_75_145)
       (c_sort ?t_5_200_144 ?y_74_146))
    ?x_75_145))))

;; Why axiom ite_false
  :assumption
    (forall (?t_6_201_147 c_type)
    (forall (?x_77_148 c_unique)
    (forall (?y_76_149 c_unique)
    (= (smtlib__ite c_Boolean_false  (c_sort ?t_6_201_147 ?x_77_148)
       (c_sort ?t_6_201_147 ?y_76_149))
    ?y_76_149))))

the proof is discharged. It makes me think that the instantiation 
process which diverges.

Where is the really origin ?

Thanks




-- 
Jean-Francois Couchot
Post Doctorant
INRIA Futurs - PROVAL
Parc club Orsay Université, Zac des Vignes
4, rue Jacques Monod, 91893 Orsay cedex
tel : (+33) (0)1 72 92 59 70 fax : (+33) (0)1 60 19 69 63