summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2014-10-06Fix a resource limiting issue where interruption didn't occur promptly. ↵Morgan Deters
Thanks Johannes Kanig for the report.
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.Morgan Deters
2014-10-06Some minor cleanup.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-06Print array constants in SMT-LIB models with new syntax.Morgan Deters
2014-10-06Clear out decls/defs with RESET command.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
Conflicts: test/regress/regress0/arrays/Makefile.am
2014-10-06Fix native language parsing of chained-store expressions (resolves bug 585). ↵Morgan Deters
Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.
2014-10-06Support for RESET command in CVC native language (and infrastructure for ↵Morgan Deters
support elsewhere).
2014-10-03Support exporting array-store-all expressions to other ExprManagers (fixes ↵Morgan Deters
portfolio test failures).
2014-10-03Merge branch '1.4.x'Morgan Deters
Conflicts: NEWS
2014-10-03Fix output of integer-valued real constants in SMT-LIB models (thanks ↵Morgan Deters
Christoph Sticksel for reporting).
2014-10-03Improve error in CVC parser in presence of unrecognized command name.Morgan Deters
2014-10-03More array constants and parsing: better error messages, extend to CVC ↵Morgan Deters
presentation language.
2014-10-03Minor fixes to CVC printer.Morgan Deters
2014-10-03SMT-LIB parser support for array constants (Z3 syntax).Morgan Deters
2014-10-02Added internal support for constant arrays.Clark Barrett
2014-10-02Merge branch '1.4.x'.Morgan Deters
2014-10-02Added option for developer use onlyClark Barrett
2014-10-02More model-based combination for arraysClark Barrett
2014-10-02Better getEqualityStatus for arrays, smarter combination of theoriesClark Barrett
2014-10-02Fix comment in SmtEngine.Morgan Deters
2014-10-02fix getModelValue(<non-preregistered term>)Kshitij Bansal
2014-10-02Fix for an array-of-record model generation assert-fail (assert was too strong).Morgan Deters
2014-10-01Option for more aggressive merging in UEE.ajreynol
2014-09-30Merge branch '1.4.x'Morgan Deters
2014-09-30Fix improper #inclusion of private header outside library.Morgan Deters
2014-09-30Fix a command-replay bug in tear-down-incremental mode. Thanks to Christoph ↵Morgan Deters
Sticksel for the report.
2014-09-30Proofs- and cores-related segfault fixes (mainly a usability issue), thanks ↵Morgan Deters
Christoph Sticksel for reporting these.
2014-09-29Add option for aggressive model filtering in conjecture generator (enumerate ↵ajreynol
ground terms).
2014-09-27Merge branch '1.4.x'Morgan Deters
2014-09-27Fix infinite loop in --bitblast-aig/--bv-aig-simp options.Morgan Deters
2014-09-26Merge branch '1.4.x'Morgan Deters
2014-09-26Fix bv options doc.Morgan Deters
2014-09-26Clarify some licensing-related things.Morgan Deters
2014-09-26Finer-grained resource-limiting in quantifiers.Morgan Deters
2014-09-26Fix AIG bitblaster for unsat cores.Morgan Deters
2014-09-25Fair datatype enumeration.ajreynol
2014-09-24Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.ajreynol
2014-09-24Refactor option for uf+cardinality constraints solver.ajreynol
2014-09-24Partial support for codatatype models.ajreynol
2014-09-23Support :no-pattern.ajreynol
2014-09-23Do not throw error when codatatype is not well-founded. Add option for ↵ajreynol
disabling codatatype reasoning. Minor cleanup.
2014-09-18Resource spending support in theories (and especially in quantifiers).Morgan Deters
2014-09-18cvc4terminate infinite loop fixKshitij Bansal
2014-09-18cvc4terminate infinite loop fixKshitij Bansal
2014-09-17Fix fix. There are no unsat cores in 1.4Kshitij Bansal
2014-09-17Merge branch '1.4.x'Kshitij Bansal
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback