Interpreter returns the unsat error for a function that runs fine and has a fp through rr

[pt7k]

1. Summary

   • Description: Bug Summary in 2 to 3 sentences.
   • As per the example in interpreter_sbf.tau demo it is possible to use functions for interpreter specifications.
   • But when a function is crafted with another one nested in it, the interpreter yields some of such examples as unsat.
   • While testing the same specification through an equivalent recurrence relation works perfectly fine.

2. Environment

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

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

sbf o1 = console
f(0) := {a}:sbf
f({a}:sbf) := 1
g(x) := {a}:sbf f(x)
r o1[0] = 0 && o1[n] = g(o1[n-1])
# interpreter fails on this, but running the same function through rr works as intended
h[0]() := 0
h[n]() := g(h[n-1]())
n h()

Step 2: Any additional input to Tau?

Expected Result
Same result from the interpreter as from the equivalent test through a recurrence relation h.
Actual Result
Interpreter:
Temporal normalization of always specification reached fixpoint after 2 steps, yielding the result:
F
(Error) Tau specification is unsat
Recurrence relation:
{ a } : sbf

4. Additional Information
   • Error Messages or Logs:
     (Error) Tau specification is unsat
   • Screenshots:

5. Severity and Impact

   • Severity Level: Minor
   • Impact on Work: Unable to use the interpreter in certain scenarios

6. Workaround (if applicable)

   • Tell us if you found a way around this problem:
   • A slightly simpler example works both ways as intended:

sbf o2 = console
f2(x) := x'
g2(x) := {a}:sbf f2(x)
h2[0]() := 0
h2[n]() := g2(h2[n-1]())
n h2()
r o2[0] = 0 && o2[n] = g2(o2[n-1])
n
n
n
q

7. Contact Information
   • Name: pt7k
   • Email: Telegram @ksdjfskfh
   • Additional Notes: Any other message for the Tau Team

Submission Instructions

• Make sure to attach any input files to this bug report.