fix for bug500
fixed bv rewrite blow-up
one more fix for rewrites
added type checking rule to check for bit-vector constants of size 0
fix for nonterminating model-based array loop
BV strategy for SMT-EVAL
fix for smt-eval run script
Fixed assertion bug
final updates for smt-eval script
update versioning
Removing arithmetic compile warning for release
Cutting release 1.2.
Merge tag 'smteval2013'
Prerelease versioning for 1.2.x
Prerelease versioning for master
Add new method for checking candidate models, --fmf-fmc.  Add infrastructure for handling bounded integer quantification (quantifiers/bounded_integers.h and .cpp).  Add option for disabling model minimality restriction for finite model finding, --disable-uf-ss-min-model.  Add option for relational triggers such as x = f(y), --relational-trigger.
Changing the integer normal form to increase matching.