summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uflia
AgeCommit message (Expand)Author
2012-06-13- Added a loop to internally assert constraints that are marked as true.Tim King
2012-06-12Fix to SMT-LIBv1 parser: QF_UF declares sort "U", but other *UF* logics do no...Morgan Deters
2012-06-12Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justificationKshitij Bansal
2012-06-11Fix to term normalization of integer equalities. Adds a regression test that ...Tim King
2012-06-11Merge from quantifiers2-trunkmerge branch.Morgan Deters
2012-06-07fixing some bugs in propagation of disequalitiesDejan Jovanović
2012-06-06Changes to the combination mechanism, lots of details. Not done yet, there ar...Dejan Jovanović
2012-05-07Fixing a bug with TheoryArith::ppAssert() and shared terms.Tim King
2012-04-17Merges branches/arithmetic/atom-database r2979 through 3247 into trunk. Belo...Tim King
2012-04-05Support to test the "dumper" mechanism in regressions (feeding dump output ba...Morgan Deters
2012-03-22some improvements to the sharing mechanism/interfaceDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback