It might be possible. Consider adding new auxiliary variables that represent the state of memory after each operation. You may be then able to add (linear) constraints to those auxiliary variables that are meaningful. Including user input could be tricky though.