Commits

Author Commit Message Labels Comments Date
Arlen Cox
New Makefile that works on Mavericks with OCaml 4.01 and is more standard anyway
Arlen Cox
Fixing missing routines. Some parsing routines appear to have been removed from Z3 and they were still in the OCaml bindings.
Arlen Cox
Merge branch 'master' of https://git01.codeplex.com/z3
Leonardo de Moura
Display version number using new format
Leonardo de Moura
New API for adding 'tracked assertions'. Added wrappers for creating existential and universal quantifiers in the C++ API fronted. Added new examples for the C++ API
Nikolaj Bjorner
add missing check for difference logic fragment for clause heads
Arlen Cox
Fixing documentation
Arlen Cox
ocamlfind library support is now complete! hooray!
Arlen Cox
Modified build files to allow compilation on Mac OS X 10.8 out of the box.
Leonardo de Moura
cleaned exampled
Leonardo de Moura
new example
Leonardo de Moura
fixed bug detected in regression tests
Leonardo de Moura
Fixed bug reported by Heizmann at codeplex
Leonardo de Moura
fixed bugs found in regression tests
Leonardo de Moura
fixed problem with Python 2.5
Nikolaj Bjorner
fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers
Leonardo de Moura
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Leonardo de Moura
resurrected test/quant_elim.cpp
Nikolaj Bjorner
set model completion to force value computation
Nikolaj Bjorner
update slicing to fix unbound variables. test datatype realizer
Nikolaj Bjorner
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Nikolaj Bjorner
fix if-lifting, added light-weight FM to qe_lite
Leonardo de Moura
minor fix for ramdisk build
Leonardo de Moura
fixed some warnings reported by clang++
Leonardo de Moura
Merge branch 'solver_na2as' into unstable
Leonardo de Moura
cleanning solver initialization, and fixing named assertion support
Leonardo de Moura
removed dead files
Leonardo de Moura
added support for named assertions
Leonardo de Moura
new qe example
Leonardo de Moura
fixed bug in solver_na2as
  1. Prev
  2. Next