Package de.uka.ilkd.key.smt.newsmt2

Failed tests

• ProveSMTLemmasTest. [2] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom
• ProveSMTLemmasTest. [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside )

Ignored tests

• MasterHandlerTest. [10] heap1.props
• MasterHandlerTest. [11] float.sqrt2.props
• MasterHandlerTest. [12] float.sinDouble.props
• MasterHandlerTest. [13] cast3.props
• MasterHandlerTest. [14] float.sqrt1.props
• MasterHandlerTest. [15] int1.props
• MasterHandlerTest. [16] quant2.props
• MasterHandlerTest. [17] float.eq.props
• MasterHandlerTest. [18] bool3.props
• MasterHandlerTest. [19] types1.props
• MasterHandlerTest. [1] ite1.props
• MasterHandlerTest. [20] cast1.props
• MasterHandlerTest. [21] quant1.props
• MasterHandlerTest. [22] cast2.props
• MasterHandlerTest. [23] ex2.props
• MasterHandlerTest. [24] types2.props
• MasterHandlerTest. [2] bool1.props
• MasterHandlerTest. [3] float2.props
• MasterHandlerTest. [4] bool2.props
• MasterHandlerTest. [5] ex1.props
• MasterHandlerTest. [6] upd2.props
• MasterHandlerTest. [7] uninterpreted1.props
• MasterHandlerTest. [8] upd1.props
• MasterHandlerTest. [9] float1.props

Classes