✧✦Catherine✦✧if SMT-LIB was designed for actually useful applications it would have had a function to replace a chunk of a bitvector with something else, instead of forcing you to do a {let binder, extract, extract, concat} dance and hope whatever you're using to emit code is flexible enough that you can actually get the let binder to work (or you end up with quadratic growth of SMT-LIB terms)
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.