search

deividrvale / CRIT

A tool for automating Rewriting Induction (RI) for Logically Constrained Term Rewriting Systems (LCTRSs)
MIT License
0 stars 1 forks source link

Z3 outputs `a!1` instead of `f` #50

Open WBrozius opened 8 months ago

WBrozius commented 8 months ago

Happens when trying to CALCULATE_SIMP on f(f(1 - 1)), starting from file 

THEORY ints     ;
LOGIC QF_LIA    ;
SOLVER internal ;

SIGNATURE f ;

RULES
    f(x) -> f(f(x - 1)) [ x > 0 ];
    f(x) -> 0 [ x <= 0 ]

QUERY equivalence f(f(f(1))) -><- 0;

END OF FILE
WBrozius commented 8 months ago

Check it out using https://compsys-tools.ens-lyon.fr/z3/index.php