Hi Tjark, Sorry, yes I mean HolSmt :) And thanks for the pointers.
Suppose I want to use a more recent version of Z3... will it be a lot of work to tweak the source code of HolSmt to achieve this? --Wish. On 7-4-2015 11:59, Tjark Weber wrote: > Dear Wishnu, > > On Tue, 2015-04-07 at 10:25 +0200, Wishnu Prasetya wrote: >> I am trying to make the HOLStmt library working on my machine. So far it >> works with Yices-1 as the back end. I have a few questions: >> >> * Does anyone know if it would work with Yices-2 ? >> * Does anyone know which Z3 version I am supposed to use for this >> HOLStmt library? > I suppose you are referring to the HolSmt library. This library is > documented in Section 5.11 of the HOL System Description, which you can > find in HOL/Manual/Description/ or download separately from > http://hol.sourceforge.net/documentation.html > > Regarding your questions, the documentation states > > | HolSmtLib has been tested with Yices 1.0.29 and Z3 2.19. Later > | versions may or may not work. (Yices 2 is not supported.) > > Best, > Tjark > > ------------------------------------------------------------------------------ BPM Camp - Free Virtual Workshop May 6th at 10am PDT/1PM EDT Develop your own process in accordance with the BPMN 2 standard Learn Process modeling best practices with Bonita BPM through live exercises http://www.bonitasoft.com/be-part-of-it/events/bpm-camp-virtual- event?utm_ source=Sourceforge_BPM_Camp_5_6_15&utm_medium=email&utm_campaign=VA_SF _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
