Undefined sort name in SMT2 when predicate argument is a struct containing a closure

[coeff-aij]

When running Thrust on a predicate that takes a struct containing a closure as an argument, the generated .smt2 file contains an undefined sort name.

• Example
  Verification target Rust code:

//@check-pass
//@compile-flags: -C debug-assertions=off

struct S<F> {
 f: F,
}

impl<F> S<F>
 where F: Fn(i32) -> i32
{
 fn apply(&self) -> i32 {
 (self.f)(1)
 }


 #[thrust::predicate]
 fn truthy(self) -> bool {
 "true"; true
 }
}

fn main() {
 let s = S {
 f: |x: i32| x + 1,
 };
 let x = s.apply();

 assert!(x == 2);
}

Thrust outputs following .smt2:

(set-logic HORN)

(declare-datatypes ((A0_Tuple<Int> 0)) (
 (par () (
 (tuple<Int> (tuple_proj<Int>.0 Int))
 ))
))

(define-fun datatype_discr<A0_Tuple<Int>> ((x A0_Tuple<Int>)) Int (ite ((_ is tuple<Int>) x) 0 (- 1)))
(define-fun matcher_pred<A0_Tuple<Int>> ((x0 Int) (v A0_Tuple<Int>)) Bool (or (= v (tuple<Int> x0))))
(define-fun S<F>_truthy ((self Tuple<T0>)) Bool true)


; span=refine_fn_def 

; --snip--

The predicate truthy is encoded as
(define-fun S<F>_truthy ((self Tuple<T0>)) Bool true)
in above, which causes unknown sort error.

 INFO thrust::chc::solver: spawned program="z3" args=["fp.spacer.global=true", "fp.validate=true"] path=/tmp/thrust_tmp_gWhJne.smt2 pid=73582
 INFO thrust::chc::solver: waiting timeout=Some(30s) pid=73582
 INFO thrust::chc::solver: exited status=exit status: 1 elapsed=12.72485ms
error: verification error: Error { stdout: "(error \"line 11 column 31: invalid sorted variables: unknown sort 'Tuple<T0>'\")\nsat\n", stderr: "" }

error: aborting due to 1 previous error