Right now unused variables are treated as assertions, e.g., this fails:

_ : (x y : ℤ) → x ≤ x  -- Unrecognized identifier Agda.Builtin.Int.Int in script "(assert Agda.Builtin.Int.Int)"

Maybe a better heuristic is to try decoding every element both as a sort and as a term and pick whichever succeeds. It would also be useful to just drop uninterpretable assumptions, so that you can use solveZ3 deep in a term with a lot of junk in the context.

It doesn't seem straightforward to do this at the moment because of the current architecture that produces a RawScript at a stage where the theory-specific decoding functions aren't available.

I tried to install the lower bounds of the suggestions in the README:
Agda (>= 2.6.2-60564a4)
agda-stdlib (>= experimental-d66a21f)
agdarsec (>= master-b26230)

But I get this error:

agda-stdlib/src/Data/List/Membership/Propositional/Properties.agda:17,1-52
Failed to solve the following constraints:
Check definition of to∘from : {P.A.a : Level} {P.A : Set P.A.a}
{P.p : Level} {P = P₁ : Pred P.A P.p} {Q.A.a : Level}
{Q.A : Set Q.A.a} {Q.p : Level} {Q = Q₁ : Pred Q.A Q.p}
{xs = xs₁ : List P.A} {ys = ys₁ : List Q.A}
(pq
: Any (λ x → Any (λ y → Prod.Σ (P₁ x) (λ x₁ → Q₁ y)) ys₁) xs₁) →
Any-×⁺ (Any-×⁻ pq) ≡ pq
stuck because
agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda:266,3-34
I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
lhs ≟ Any.map
(λ x →
Any.map (λ q → P.subst P x p , q)
(Any.map
(λ x₁ →
P.subst Q x₁
(_5428 (x = x₂) (pq′ = pq′) (y = y) (y∈ys = y∈ys) (p = p) (q = q)
(lem₂ = lem₂) (pq = pq) (x∈xs = x∈xs) (lem₁ = lem₁)
(p = (P.subst P x p))))
y∈ys))
x∈xs
when checking that the pattern refl has type
lhs ≡
Any.map
(λ x →
Any.map (λ q → P.subst P x p , q)
(Any.map
(λ x₁ →
P.subst Q x₁
(_5428 (x = x₂) (pq′ = pq′) (y = y) (y∈ys = y∈ys) (p = p) (q = q)
(lem₂ = lem₂) (pq = pq) (x∈xs = x∈xs) (lem₁ = lem₁)
(p = (P.subst P x p))))
y∈ys))
x∈xs
(blocked on _P.p_475)
when scope checking the declaration
open import Data.List.Relation.Unary.Any.Properties
agda-stdlib/src/Data/List/Membership/Propositional/Properties.agda:17,1-52
Unsolved metas at the following locations:
agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda:100,17-18
agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda:105,16-17
agda-stdlib/src/Data/List/Relation/Unary/Any/Properties.agda:105,28-29
when scope checking the declaration
open import Data.List.Relation.Unary.Any.Properties

I also tried the upper bounds - i.e., the latest versions

I get this error:

schmitty/src/Text/Parser/String.agda:53,17-31
Not in scope:
Parser.Success
at schmitty/src/Text/Parser/String.agda:53,17-31
(did you mean 'Success'?)
when scope checking Parser.Success

agda/agda-stdlib@c49854d#diff-e0f22a07a1e767e68cb3581868064af185b9557ffbf50917c8668c9ad61b1f14 leads to the error

~/work/schmitty-master/src/Data/List/Relation/Binary/Subset/Propositional/ExtraProperties.agda:22,1-10
Multiple definitions of xs⊆xs++ys. Previous definition at
~/work/agda-stdlib-experimental/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda:139,1-10
when scope checking the declaration
 xs⊆xs++ys : xs ⊆ xs ++ ys

at least on the current state of the experimental standard library.

Also, schmitty's readme says the standard library should be at least agda/agda-stdlib@da286d0 but the link agda/agda-stdlib@9c56155 is for an earlier pull request. In both cases, I get the error

~/work/agda-stdlib/src/Reflection/Term.agda:392,20-26
Too few arguments to constructor absurd, expected 1 more explicit
argument
when checking that the pattern absurd has type Pattern

I am not sure how to proceed in trying to get the tests to run. I appreciate any advice!

The tests which return a model are not robust. For instance:

script : Script [] (REAL ∷ REAL ∷ []) (MODEL (REAL ∷ REAL ∷ []) ∷ [])
script = declare-const "x" REAL
       ∷ declare-const "y" REAL
       ∷ assert (app₂ eq (# 0) (app₂ div (# 1) (lit (nat 2))))
       ∷ assert (app₂ gt (# 0) (lit (nat 1)))
       ∷ assert (app₂ gt (# 1) (lit (nat 1)))
       ∷ get-model
       ∷ []

_ : z3 script ≡ ((sat , 1.5 ∷ 3.0 ∷ []) ∷ [])
_ = refl

These tests are currently written on a by-solver basis, under the assumption that the returned models may differ between solvers, but are deterministic for a single solver. Unfortunately, this is not the case. Therefore, these tests have to be migrated to tests which check the asserted properties, i.e., for the test case above, we should check that z3 script ≡ ((sat , x ∷ y ∷ []) ∷ []) where x ≡ y / 2.