refactor away some duplication
add support for select instructions
bugfixing
missing type constraint for select
print all vars of source and target on counterexample
fix bug with handling '%B = cnst'
add support for undefined values
This commit introduces proofs with quantified variables, which is potentially
expensive to reason with. Need testing with different Z3 solvers
refactor code to support pointer types
WIP
add support for generating SMT-LIB 2 benchmarks
add concept of state
State is a valution from registers and memory locations to concrete values
This is required for next commits that will introduce memory access instructions, which
have sequence.
This commit has the side-effect of speeding up verification of larger optimizations,
since the SMT expressions of each register are now cached
ensure all alloca'd pointers are distinct
stub out load+store instructions
stub out axiomatization of memory model
The model is pretty complete, modulo bugs, alignments, etc.  The model allows conversion
from pointers to integers and back
improve support for memory. WIP.
fix regression
add support for portfolio SMT solving
We will now pick specialized solvers from Z3 depending on whether there are qantifiers
or not
This change improves predicatbility of running time, and should improve performance for
larger tests as a side-effect.
Thanks to Santosh Nagarakatte for reporting the performance issue.
add preliminary support for inttopr, ptrtoint, and bitcast
optimize type constraints for TypeFixedValues
bug fixes to memory handling instructions
validate final memory state as part as the verification process
improve error messages
preliminary support for getelementptr