| add test case for substitution |
|
More...
|
almost 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
almost 12 years ago
|
| fix default argument identification |
|
More...
|
almost 12 years ago
|
| address incompleteness bug in axiomatization of int2bv |
|
More...
|
almost 12 years ago
|
| fix bugs reported by Anvesh |
|
More...
|
almost 12 years ago
|
| test for undetermined accessor for PDR |
|
More...
|
almost 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
almost 12 years ago
|
| check equalities with unknown evaluations |
|
More...
|
almost 12 years ago
|
| Reorganized the SLS code. |
|
More...
|
almost 12 years ago
|
| qfbv-sls tactic bugfix |
|
More...
|
almost 12 years ago
|
| redo edit |
|
More...
|
almost 12 years ago
|
| something cl was complaining about |
|
More...
|
almost 12 years ago
|
| Merge /home/mcmillan/projects/z3_interp into interp |
|
More...
|
almost 12 years ago
|
| fix lemma counting and nix NEW_EXTRACT_TH_LEMMA |
|
More...
|
almost 12 years ago
|
| still working on interpolation of full z3 proofs |
|
More...
|
almost 12 years ago
|
| cycle through domain size before giving up |
|
More...
|
almost 12 years ago
|
| patching crash in data-type factory when fresh values are not produced |
|
More...
|
almost 12 years ago
|
| Fix build of test |
|
More...
|
almost 12 years ago
|
| fix bug found by Ethan: fresh values for bit-vectors loops if the domain of bit-vectors is truly small |
|
More...
|
almost 12 years ago
|
| remove some dependencies on parameter file |
|
More...
|
almost 12 years ago
|
| testing qe_arith |
|
More...
|
almost 12 years ago
|
| update test in qe_arith |
|
More...
|
almost 12 years ago
|
| fixes for qe_arith |
|
More...
|
almost 12 years ago
|
| add qe_arith routine for LW projection on monomomes |
|
More...
|
almost 12 years ago
|
| check for uninterpreted functions in tail for PDR |
|
More...
|
almost 12 years ago
|
| partition inequalities into conjuncts determined by equivalence classes of shared variables |
|
More...
|
almost 12 years ago
|
| fix C(R) |
|
More...
|
almost 12 years ago
|
| Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable |
|
More...
|
almost 12 years ago
|
| add transformation to reduce overhead of negation for predicates with free variables |
|
More...
|
almost 12 years ago
|
| add const qualifiers to fix warning messages |
|
More...
|
almost 12 years ago
|
