projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e772896) | patch
Minor fix to avoid rewriting datatype equalities into non-equalitiers, as required...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Apr 2014 08:16:56 +0000 (03:16 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Apr 2014 08:16:56 +0000 (03:16 -0500)
commit766859010a5ca2cc94ffe69908dfe2606df2af28
tree09298c96c3cf547b68fba87bff22ba654d9afef1tree
parente77289614a61d8658f8fc56073fa3334c14139b8commit | diff
Minor fix to avoid rewriting datatype equalities into non-equalitiers, as required.  Add APPLY_UF to congruence types to avoid model construction bugs.
src/theory/datatypes/datatypes_rewriter.h diff | blob | history
src/theory/datatypes/theory_datatypes.cpp diff | blob | history