There are a few missing necessities in patsolve_smt2

[chemoelectric]

patsolve_smt2 ought to have definitions for assign_ifint_bool_int_int(), assign_int_of_addr(), assign_addr_of_int()

I have been using the following filter as a workaround (substitute your favorite Awk):

#!${POSIX_AWK} -f

-- mode: awk; coding: utf-8 --

Copyright (C) 2019 Barry Schwartz

This file is part of ATS2 Patstrans.

ATS2 Patstrans is free software: you can redistribute it and/or

modify it under the terms of the GNU General Public License

as published by the Free Software Foundation, either version 3 of

the License, or (at your option) any later version.

ATS2 Patstrans is distributed in the hope that it will be useful,

but WITHOUT ANY WARRANTY; without even the implied warranty of

MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU

General Public License for more details.

You should have received a copy of the GNU General Public

License along with ATS2 Patstrans. If not, see

http://www.gnu.org/licenses/.

BEGIN {

FIXME: The following SMT2 function definitions should be

inserted by patsolve_smt2, but you can use this filter to

work around it if they are not.

assign_ifint_bool_int_int()
assign_int_of_addr()
assign_addr_of_int()
}

{
if (/^[[:space:]]*([[:space:]]declare-fun[[:space:]]+/)
{
fun_name = $0
gsub (/^[[:space:]]([[:space:]]declare-fun[[:space:]]+/, "", fun_name)
gsub (/[^[:alpha:]_0-9].$/, "", fun_name)
for (f in fun)
if (fun_name ~ f)
{
print neaten(fun[f])
next
}
}
print $0
}

function neaten(s)
{
gsub(/[[:space:]][[:space:]]+/, " ", s)
return s
}

function assign_ifint_bool_int_int()
{
fun["^ifint_bool_int_int$"] =
"(define-fun ifint_bool_int_int ((b Bool) (i1 Int) (i2 Int)) Int "
" (ite b i1 i2))"
}

function assign_int_of_addr()
{
fun["^int_of_addr$"] =
"(define-fun int_of_addr ((p Int)) Int p)"
}

function assign_addr_of_int()
{
fun["^addr_of_int$"] =
"(define-fun addr_of_int ((p Int)) Int p)"
}

[chemoelectric]

You can get a clean copy of that filter at https://bitbucket.org/ats2libraries/mats2-integers/src/default/patstrans_smt2_filter.in :)

(I mostly prove theorems in ATS2 for fun, which is why I needed that. BTW I think CVC4 works a lot better than does Z3.)