Automated Analysis of Logically Constrained Rewrite Systems using crest

Abstract

Abstract We present , a tool for automatically proving (non-) confluence and termination of logically constrained rewrite systems. We compare to other tools for logically constrained rewriting. Extensive experiments demonstrate the promise of .