Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)

Kanta Takahata, Jonas Schöpf, Naoki Nishida +1

Logically constrained term rewriting is a relatively new rewriting formalism that naturally supports built-in data structures, such as integers and bit vectors. In the analysis of…