projects / cvc5.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
cvc5.git
2012-11-29 Clark BarrettFix for nasty corner case found by fuzzer... commit | commitdiff | tree
2012-11-29 Kshitij BansalHack to support global variables for CVC language exten... commit | commitdiff | tree
2012-11-29 Clark BarrettFixing function models with Boolean terms. Also, LAMBD... commit | commitdiff | tree
2012-11-28 Tim KingAdding the helloworld.cpp example. commit | commitdiff | tree
2012-11-28 Kshitij Bansalfix a potential race (have failed to reproduce) commit | commitdiff | tree
2012-11-28 Clark BarrettFix for getValue. Now it can handle lambda applications commit | commitdiff | tree
2012-11-28 Morgan DetersAttempted "quick-fix" for QF_UF performance regression... commit | commitdiff | tree
2012-11-28 Kshitij Bansaltreat all get commands like getValue (send only to... commit | commitdiff | tree
2012-11-28 Kshitij Bansalminor commit | commitdiff | tree
2012-11-28 Morgan Detersupdate to release notes commit | commitdiff | tree
2012-11-28 Morgan DetersBug fix: commit | commitdiff | tree
2012-11-28 Morgan Detersfix: correct misleading comment in dump output commit | commitdiff | tree
2012-11-27 Morgan DetersFunctions and predicates over Boolean now work with... commit | commitdiff | tree
2012-11-27 Kshitij Bansalfix in CommandSequence invoke : maintain success/failur... commit | commitdiff | tree
2012-11-27 Morgan Detersmore mac fixes commit | commitdiff | tree
2012-11-27 Morgan Detersfix for some Mac builds commit | commitdiff | tree
2012-11-27 Kshitij BansalSimplify --help=decision with only currently supported... commit | commitdiff | tree
2012-11-27 Morgan Detersgive warning at configure-time about unsupported langua... commit | commitdiff | tree
2012-11-27 Morgan Detersdo not turn on BV for QF_SAT commit | commitdiff | tree
2012-11-27 Morgan DetersFirst chunk of boolean-terms support. commit | commitdiff | tree
2012-11-27 Morgan DetersTuples and records merge. Resolves bug 270. commit | commitdiff | tree
2012-11-27 Tim KingAdding an example to show how to use arithmetic. commit | commitdiff | tree
2012-11-26 Tim KingImproved implementation of Integer::length() with CLN... commit | commitdiff | tree
2012-11-26 Morgan Detersinclude new regression directories in summary test... commit | commitdiff | tree
2012-11-26 Morgan Detersrolling back r4625 for now (closes bug 464), Andy we... commit | commitdiff | tree
2012-11-26 Dejan Jovanovićfixup for incremental solving commit | commitdiff | tree
2012-11-26 Tim KingRemoving DioSolver::acceptableOriginalNodes(). This... commit | commitdiff | tree
2012-11-26 Dejan JovanovićAdding support for a master equality engine. Each theor... commit | commitdiff | tree
2012-11-26 Tim KingImproving arithmetic debugging output. commit | commitdiff | tree
2012-11-26 Tim KingDisabling test/regress/regress0/push-pop/bug396.smt2... commit | commitdiff | tree
2012-11-26 Morgan Detersdon't include internal variables in model output commit | commitdiff | tree
2012-11-26 Morgan Deterssome fixes to language bindings and function visibility commit | commitdiff | tree
2012-11-26 Morgan DetersMakefile fix for new versions of Make (thanks Clark... commit | commitdiff | tree
2012-11-25 Tim KingAdding a regression test from bug 462. commit | commitdiff | tree
2012-11-25 Tim KingThis commit fixes two incompleteness bugs (461, 459... commit | commitdiff | tree
2012-11-24 Tim KingAdds ensureConstraint(...) to ConstraintDatabase. This... commit | commitdiff | tree
2012-11-23 François BobotExample of rewrite rules use that comes from an harness... commit | commitdiff | tree
2012-11-21 Tim King- Removes getDeltaValueWithNonlinear() entirely commit | commitdiff | tree
2012-11-21 Tim KingAdds a number of new capabilities to DeltaRational... commit | commitdiff | tree
2012-11-21 Tim KingAdded debugging output to --check-models. I've found... commit | commitdiff | tree
2012-11-19 Kshitij BansalRun lastWinner thread for all commands. Earlier behavio... commit | commitdiff | tree
2012-11-19 Tim KingAdding hand minimized test for bug 450. commit | commitdiff | tree
2012-11-19 Tim KingChanged the splitting-on-demand lemmas of arithmetic... commit | commitdiff | tree
2012-11-19 Tim KingFix for bug452. commit | commitdiff | tree
2012-11-18 Morgan DetersDisable predicate subtyping: commit | commitdiff | tree
2012-11-18 Andrew Reynoldssupport for quantifiers macros, bug fix for bug 454... commit | commitdiff | tree
2012-11-17 Clark BarrettFixed last currently known bug in array models commit | commitdiff | tree
2012-11-17 Morgan Deters* enable previously-failing (now succeeding) datatype... commit | commitdiff | tree
2012-11-17 Morgan Detersfix for language bindings (fixes debian build fail... commit | commitdiff | tree
2012-11-17 Morgan Deters* Fix for bug 445 agreed to in meeting 11/13/2012:... commit | commitdiff | tree
2012-11-16 Clark BarrettFix for bug451 commit | commitdiff | tree
2012-11-16 Dejan Jovanovićfixing and refactoring the equality iterator commit | commitdiff | tree
2012-11-16 Morgan DetersFix dumping of array-select expressions in CVC native... commit | commitdiff | tree
2012-11-16 Morgan Detersfix a compiler warning in models commit | commitdiff | tree
2012-11-15 Kshitij Bansalsome fixes for --threads=1 commit | commitdiff | tree
2012-11-15 Morgan Detersfix for "make examples" commit | commitdiff | tree
2012-11-15 Clark BarrettMore fixes to model generation, with previously failing... commit | commitdiff | tree
2012-11-15 Liana Hadareanforgot to uncomment setLogicInternal for THEORY_BV commit | commitdiff | tree
2012-11-15 Liana Hadareanchanged logic options so that justification is turned... commit | commitdiff | tree
2012-11-15 Morgan Detersd_incomplete is context-dependent; we shouldn't be... commit | commitdiff | tree
2012-11-15 Clark Barrettfuzz15 should have been fuzz14 commit | commitdiff | tree
2012-11-15 Tim KingFix for bug 447. commit | commitdiff | tree
2012-11-15 Clark BarrettFixed another AUFBV model bug. BV equality subtheory... commit | commitdiff | tree
2012-11-15 Tim KingFixing comments in print_lambda.cvc. commit | commitdiff | tree
2012-11-14 Tim KingFix for bug 407. mkAnonymousFunction() in the parser... commit | commitdiff | tree
2012-11-14 Andrew Reynoldsreplaced all static member data from rewrite rule trigg... commit | commitdiff | tree
2012-11-14 Tim KingFixed a typo in r4576 commit | commitdiff | tree
2012-11-14 Tim KingBeautifying smt_engine.cpp. commit | commitdiff | tree
2012-11-14 Tim KingFix to bug449. Adds shared constants to the set of... commit | commitdiff | tree
2012-11-14 Clark Barrettbug fixes to models, array rewriter with previously... commit | commitdiff | tree
2012-11-14 Kshitij BansalQuantifiers enabled with portfolio, closing bug 423. commit | commitdiff | tree
2012-11-14 Kshitij Bansalfix a race problem. due to interrupt mechanism minisat... commit | commitdiff | tree
2012-11-13 Clark BarrettMore bugfixes for models commit | commitdiff | tree
2012-11-13 Tim KingSmtEngine::checkModel() should only be called if the... commit | commitdiff | tree
2012-11-13 Andrew Reynoldsrefactoring of quantifiers rewriter based on code revie... commit | commitdiff | tree
2012-11-13 Liana Hadareanfixed failed bv regressions by refactoring out some... commit | commitdiff | tree
2012-11-13 Liana Hadareanadded support for division by zero for bit-vector divis... commit | commitdiff | tree
2012-11-13 Clark BarrettRelaxing too-strict assertion commit | commitdiff | tree
2012-11-13 Clark BarrettFixed an array rewriting bug found by fuzzer commit | commitdiff | tree
2012-11-13 Clark BarrettTestcases for fixed bugs commit | commitdiff | tree
2012-11-13 Clark BarrettFixed bug in array constant normalization found by... commit | commitdiff | tree
2012-11-12 Tim KingImproved error reporting for improperly using non-linea... commit | commitdiff | tree
2012-11-12 Tim KingDelta is now generated in arithmetic to keep consistent... commit | commitdiff | tree
2012-11-12 Liana Hadareanchanged BitVector::unsignedRem to match the behavior... commit | commitdiff | tree
2012-11-12 Morgan DetersFix for bug 444, dealing with the placing of set-logic... commit | commitdiff | tree
2012-11-12 Morgan Deters* Fix language bindings: various issues commit | commitdiff | tree
2012-11-12 Andrew Reynoldsminor bug fixes for quantifiers, added sort inference... commit | commitdiff | tree
2012-11-11 Tim KingFixes for the arithmetic normal form and rewriter to... commit | commitdiff | tree
2012-11-10 Tim KingBeautifying integer_cln_imp.h commit | commitdiff | tree
2012-11-10 Tim KingFix to quantifier rewritting not being idempotent.... commit | commitdiff | tree
2012-11-10 Tim KingRemoving rewriter call in SmtEngine::addFormula(). commit | commitdiff | tree
2012-11-10 Clark BarrettFixed missing \ in uflra/Makefile.ma commit | commitdiff | tree
2012-11-10 Tim KingFix for bug 439. Delta computation now includes disequa... commit | commitdiff | tree
2012-11-10 Morgan DetersChange run-regression script to *additionally* run... commit | commitdiff | tree
2012-11-10 Morgan DetersUpdates to Clark's commit r4540: commit | commitdiff | tree
2012-11-10 Morgan Detersfix typo in language bindings commit | commitdiff | tree
2012-11-10 Clark BarrettFinally tracked down problems in regressions and fuzz... commit | commitdiff | tree
2012-11-09 Morgan DetersTheoryEngineModelBuilder::buildModel() is only called... commit | commitdiff | tree
2012-11-09 Kshitij Bansalexport null nodes (fixes a bug in portfolio model stuff) commit | commitdiff | tree
2012-11-09 Tim KingTest that breaks arithmetic model building due to diseq... commit | commitdiff | tree
next