summaryrefslogtreecommitdiff
path: root/test/regress/regress0/aufbv/fuzz02.smt
AgeCommit message (Collapse)Author
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313.
2012-06-12bufixes and the bugsDejan Jovanović
* array now only propagates thropugh the equality engine * assertions in the equality rewriting to ensure eq -> { eq, T, F }
2012-06-11some failing examplesDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback