Solver not working with functions

[pt7k]

1. Summary

   • The solver does not find solutions to any sbf functions.
   • It also fails to translate bv functions to cvc5.

2. Environment

   • Tau Version: for now "v0.7-alpha"
   • Build Number or Date: b87a0e7
   • Operating System: Ubuntu

3. Steps to Reproduce
   Step 1: What input did you first provide?

f(x:sbf) := x:sbf
g(y:bv) := y:bv
solve f(x:sbf) = 1
solve f(1) = x:sbf
solve g(y:bv) = {2}:bv
solve g({2}:bv) = y:bv

**Expected Result**

tau> solve f(x:sbf) = 1
solution: {
	x := {1}::sbf
}

tau> solve f(1) = x:sbf
solution: {
	x := {1}::sbf
}

tau> solve g(y:bv) = {2}:bv
solution: {
	y := { 2 }:bv[16]
}

tau> solve g({2}:bv) = y:bv
solution: {
	y := { 2 }:bv[16]
}

**Actual Result**

tau> solve f(x:sbf) = 1
no solution

tau> solve f(1) = x:sbf
solution: {
	x := f(1)
}

tau> solve g(y:bv) = {2}:bv
(Error) Failed to translate the formula to cvc5: g(y) = { 2 }:bv[16]
no solution

tau> solve g({2}:bv) = y:bv
(Error) Failed to translate the formula to cvc5: g({ 2 }:bv[16]) = y
no solution

4. Additional Information
   • Error Messages or Logs:
   • (Error) Failed to translate the formula to cvc5: g(y) = { 2 }:bv[16]
   • (Error) Failed to translate the formula to cvc5: g({ 2 }:bv[16]) = y
   • Screenshots:
   • Current builds:

• Older builds:

7. Contact Information
   • Name: pt7k
   • Email: Telegram @ksdjfskfh