Add simplification rule for byte lost in >>

Can help for instance to reduce complexity when a word is used as a
shift buffer for bytes.
Add check_concolic_value debug routine

Add some code to check on the fly whether for each newly generated
temporary subformula, the concolic value of the subformula is
satisfiable under the path condition. This kind of check can help
track down places where the path condition is unexpectedly diverging
from the concolic input, or potentially if the formula construction
is making a mistake.

No command line option to enable it yet, since I don't know how
broadly useful it will be. For now, you just need to uncomment it.
Added push/pop support to the SMTLIB2 interface

Original patch from Matt Morehouse, but hand-applied because of
(whitespace?) divergences.

From 2f1873f846ce5bfe4731c27667c5122fc2d095e4 Mon Sep 17 00:00:00 2001
From: Matt Morehouse <mattmorehouse@gmail.com>
Date: Wed, 8 Oct 2014 10:09:36 -0500
Subject: [PATCH] Added push/pop support to the SMTLIB2 interface
Generalize SMTLIB2 support for CVC4

Original patch from Matt Morehouse, but hand-applied and further
changes: seemingly missing options_solver changes, rename_var for
re-flipping counterexample variable names.
The -stp-path option is now -solver-path, though the old name is
still recognized.
Merge remote-tracking branch 'upstream/master'