Commits

Author Commit Message Labels Comments Date
Leonardo de Moura
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Leonardo de Moura
updated release notes Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Nikolaj Bjorner
updated comments to create_children Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
qe-lite Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
remove dead code Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
working on symbolic execution for PDR Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
working on symbolic execution for PDR Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Leonardo de Moura
fixed update_api.py Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
Renamed z3_dbg.dll to z3.dll Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
Fixed bug in DLL .def generation Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
Extending public API with internal objects Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
fixed update_api.py Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Leonardo de Moura
Simplified binding and logging support generation. Now, everything is generated by update_api.py script. The binding commands can be included in the .h files (e.g., z3_api.h Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
working on expansion Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
working on symbolic execution trace unfolding Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
Add coalesce transformer Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
add rule unfolding transformation Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
finish (inefficient) BMC for non-linear Horn Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
finish (inefficient) BMC for non-linear Horn Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Leonardo de Moura
Merge branch 'working' of //z3-1/z3 into working
Leonardo de Moura
Added support for parsing negative numerals in the SMT 2.0 frontend Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
optimize model pruning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
optimize model pruning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
working on pdr Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
working on pdr Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
optimize model pruning Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Nikolaj Bjorner
Merge branch 'working' of https://z3-1/gw/git/z3 into working
Leonardo de Moura
goodies for gdb Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
Nikolaj Bjorner
Merge branch 'working' of https://z3-1/gw/git/z3 into working
  1. Prev
  2. Next