Author Commit Message Labels Comments Date
Default avatar Arlen Cox
New Makefile that works on Mavericks with OCaml 4.01 and is more standard anyway
Arlen Cox avatarArlen Cox
Fixing missing routines. Some parsing routines appear to have been removed from Z3 and they were still in the OCaml bindings.
Arlen Cox avatarArlen Cox
Merge branch 'master' of https://git01.codeplex.com/z3
Leonardo de Moura avatarLeonardo de Moura
Display version number using new format
Leonardo de Moura avatarLeonardo 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 avatarNikolaj Bjorner
add missing check for difference logic fragment for clause heads
Arlen Cox avatarArlen Cox
Fixing documentation
Arlen Cox avatarArlen Cox
ocamlfind library support is now complete! hooray!
Arlen Cox avatarArlen Cox
Modified build files to allow compilation on Mac OS X 10.8 out of the box.
Leonardo de Moura avatarLeonardo de Moura
cleaned exampled
Leonardo de Moura avatarLeonardo de Moura
new example
Leonardo de Moura avatarLeonardo de Moura
fixed bug detected in regression tests
Leonardo de Moura avatarLeonardo de Moura
Fixed bug reported by Heizmann at codeplex
Leonardo de Moura avatarLeonardo de Moura
fixed bugs found in regression tests
Leonardo de Moura avatarLeonardo de Moura
fixed problem with Python 2.5
Nikolaj Bjorner avatarNikolaj Bjorner
fix model completion bug in PDR, addhoc handling of reals for arithmetic realizers
Leonardo de Moura avatarLeonardo de Moura
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Leonardo de Moura avatarLeonardo de Moura
resurrected test/quant_elim.cpp
Nikolaj Bjorner avatarNikolaj Bjorner
set model completion to force value computation
Nikolaj Bjorner avatarNikolaj Bjorner
update slicing to fix unbound variables. test datatype realizer
Nikolaj Bjorner avatarNikolaj Bjorner
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
Nikolaj Bjorner avatarNikolaj Bjorner
fix if-lifting, added light-weight FM to qe_lite
Leonardo de Moura avatarLeonardo de Moura
minor fix for ramdisk build
Leonardo de Moura avatarLeonardo de Moura
fixed some warnings reported by clang++
Leonardo de Moura avatarLeonardo de Moura
Merge branch 'solver_na2as' into unstable
Leonardo de Moura avatarLeonardo de Moura
cleanning solver initialization, and fixing named assertion support
Leonardo de Moura avatarLeonardo de Moura
removed dead files
Leonardo de Moura avatarLeonardo de Moura
added support for named assertions
Leonardo de Moura avatarLeonardo de Moura
new qe example
Leonardo de Moura avatarLeonardo de Moura
fixed bug in solver_na2as
  1. Prev
  2. Next
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.