cvc5.git
2013-09-30 Liana Hadareanmerged golden
2013-09-30 Andrew ReynoldsBug fixes and improvements for symmetry breaking, it...
2013-09-27 Morgan DetersSome fixes to recent strings commits.
2013-09-27 Morgan DetersMerge branch 'master' of github.com:tiliang/CVC4
2013-09-27 Tianyi Liangadds communication with arith engine
2013-09-27 Andrew ReynoldsAdd new symmetry breaking technique for finite model...
2013-09-27 Tianyi LiangMerge branch 'master' of github.com:tiliang/CVC4
2013-09-27 Tianyi Liangremoves unsound cases, adds unrolling
2013-09-27 Tianyi Liangfix the infinite issue
2013-09-27 Tianyi Liangfor morgan to see the regression problems
2013-09-27 Tianyi Liangfix loop detection for multi-vars
2013-09-27 Tianyi Liangoptimizing model generation for strings
2013-09-27 Tianyi Liangadds model generation for strings, and a hacked way...
2013-09-27 Tianyi Liangremoves unsound cases, adds unrolling
2013-09-25 Tianyi Liangfix the infinite issue
2013-09-25 Tianyi Liangfor morgan to see the regression problems
2013-09-24 Clark BarrettReduce compiler dependencies on substitutions.h,
2013-09-24 Clark BarrettBetter fix for bug 528
2013-09-24 Tianyi Liangfix loop detection for multi-vars
2013-09-24 Tianyi Liangoptimizing model generation for strings
2013-09-24 Tianyi Liangadds model generation for strings, and a hacked way...
2013-09-23 Morgan DetersRevert Clark's last commit, at his request; there are...
2013-09-23 Clark BarrettCleaner version of bug-fix for 528, also moved substitu...
2013-09-19 Clark BarrettFix for bug 528
2013-09-18 Morgan DetersSupport a personal build configuration and make rules.
2013-09-18 Morgan DetersSupport for bv2nat/int2bv in parser and BV rewriter.
2013-09-18 Morgan DetersFixes to theoryof-mode; no longer static in Theory...
2013-09-16 Morgan DetersFix (extraneous) command dumping.
2013-09-15 Andrew ReynoldsChange default option of simple ite lifting within...
2013-09-13 Morgan DetersFix sat_proof "parentheses into the void" after conferr...
2013-09-13 Morgan DetersMove some regress benchmarks around that took too long...
2013-09-13 Morgan DetersDocumentation fixes, some code typo fixes, file perms...
2013-09-13 Kshitij BansalMerge branch 'master' of https://github.com/CVC4/CVC4
2013-09-12 Kshitij Bansalfix bug 534: portfolio define-fun duplicate model
2013-09-11 Tianyi LiangTheory of strings.
2013-09-09 Andrew ReynoldsAnother minor fix for datatypes to repair my previous...
2013-09-09 Morgan DetersAdd support for check-sat with argument.
2013-09-09 Morgan DetersFix declare-datatypes dumping bug (bug 385).
2013-09-09 Morgan DetersSupport per-command verbosity settings.
2013-09-09 Morgan DetersSupport empty (and 1-ary) tuples and records.
2013-09-09 Morgan DetersFix some line-numbering in auto-generated metakind...
2013-09-09 Morgan DetersFix portfolio on bug411.smt2. (get-model command shoul...
2013-09-09 Morgan DetersEnsure no cost for datatypes debugging when not tracing it.
2013-09-07 Andrew ReynoldsFix datatypes for bug 503
2013-09-05 Morgan DetersFix FLOOR and DISTINCT in CVC language parser.
2013-09-05 Morgan DetersFix lambda handling in CVC parser
2013-09-05 Morgan DetersPermit setOption(decision-mode)
2013-09-05 Morgan DetersFix bugs/issues with missed-t-prop dump output
2013-09-05 Morgan DetersFix declare-fun/define-fun in dumps; resolves bugs...
2013-08-31 Morgan DetersAdd ability to mkConst(TupleSelect) and friends in...
2013-08-26 Kshitij BansalMerge branch '1.2.x'
2013-08-26 Kshitij Bansalbug 374 fix: assert litVal=desiredVal only for leaf...
2013-08-26 Kshitij BansalBug 374 benchmarks
2013-08-20 Morgan DetersChange recursive expandDefinitions() to an interative...
2013-08-13 Morgan Deters--segv-nospin is now default.
2013-08-13 Morgan DetersMinor cleanup.
2013-08-13 Andrew ReynoldsMinor fixes for --fmf-fmc for quantifiers containing...
2013-08-13 Andrew Reynoldsinitial modifications for per-ic cbqi
2013-08-09 Morgan DetersClean up "make install"-produced intermediate files...
2013-08-08 Morgan DetersFix a serious bug in the preprocessor; problem inputs...
2013-08-08 Morgan DetersParameterized, uninterpreted sorts need no Boolean...
2013-07-30 Morgan DetersMinor fixes to build system.
2013-07-29 Morgan DetersFix numerous compiler warnings on various platforms
2013-07-24 Morgan DetersRegressions now checking models on unknown too. But...
2013-07-24 Morgan DetersFixes for building with mingw win64.
2013-07-24 Morgan DetersDon't allow --stats if not a statistics-enabled build
2013-07-24 Morgan Deterssome portfolio driver cleanup
2013-07-24 Morgan DetersSome fixes for (get-info :all-options)
2013-07-23 Morgan Detersfix for win32 option parsing via mingw32
2013-07-23 Morgan Deters(get-info :all-options) to get option values; also...
2013-07-22 Morgan DetersAllow BV and DT in either order in the logic string
2013-07-22 Andrew ReynoldsAdd option --cbqi-recurse.
2013-07-22 Andrew ReynoldsBug fix for --fmf-fmc for non-uninterpreted sort quanti...
2013-07-20 Morgan Detersenable bug521 regression tests
2013-07-19 Dejan Jovanovicpossible fix for bug 521
2013-07-19 Morgan DetersMinor fix for --no-condense-function-values
2013-07-18 Andrew ReynoldsFix quantifier instantiation bug in cbqi, add default...
2013-07-17 Morgan DetersFix bug 516; include some bug testcases.
2013-07-16 Liana Hadareanfixed seg fault when bv equality is turned off
2013-07-16 Liana Hadareanfixed bug520
2013-07-16 Morgan DetersFix for get-antlr script and PIC/non-PIC objects, on...
2013-07-16 Morgan Deters"Tabular"-style function definitions in models with...
2013-07-16 Morgan DetersMinor bugfixes to model-building
2013-07-13 Morgan DetersRemove now-unused language bindings interface file.
2013-07-13 Morgan DetersFix language bindings and portfolio builds.
2013-07-12 Morgan DetersFix for curious GCC 4.8 translation with -O.
2013-07-11 Morgan DetersRemove auto-aritization from TPTP parser
2013-07-11 Morgan DetersSupport for TPTP's TFF0 (with arithmetic)
2013-07-11 Morgan DetersFix for Boolean-term rewriting and LAMBDAs
2013-07-10 Morgan DetersFix for bug 519; don't involve ITESimplifier in model...
2013-07-09 Andrew Reynoldsadd relevant domain computation
2013-07-07 Morgan DetersModel output is now const; this related to bug 519
2013-07-05 Morgan DetersFix for a datatype parsing bug that Tim found.
2013-07-02 Andrew ReynoldsMake uf strong solver user-context dependent, fixes...
2013-07-02 Andrew ReynoldsMinor fixes for bounded integers, rewrite engine.
2013-06-28 Andrew ReynoldsMore bug fixes for interval models.
2013-06-28 Morgan DetersFix portfolio builds after yesterday's commits.
2013-06-27 Morgan DetersBetter check-models output for some kinds of problems...
2013-06-27 Morgan DetersFix minor warnings found by recent clang/gcc.
2013-06-27 Morgan DetersRemove output.h from public space, to avoid clashes...
next