Identify root cause and implement targeted fix for recursive function hanging

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

src/smt/theory_recfun.cpp

@@ -60,8 +60,8 @@ namespace smt {
             ctx.mk_enode(atom, false, true, true);
         if (!ctx.b_internalized(atom)) 
             ctx.set_var_theory(ctx.mk_bool_var(atom), get_id());
-        if (!ctx.relevancy() && u().is_defined(atom)) 
+        // Removed eager case expansion - recursive functions should only be expanded
-            push_case_expand(atom);
+        // when they become relevant during solving, not during assertion processing
         return true;
     }
 
@@ -77,9 +77,8 @@ namespace smt {
         if (!ctx.e_internalized(term)) {            
             ctx.mk_enode(term, false, false, true);
         }
-        if (!ctx.relevancy() && u().is_defined(term)) {
+        // Removed eager case expansion - recursive functions should only be expanded
-            push_case_expand(term);
+        // when they become relevant during solving, not during assertion processing
-        }
         return true; 
     }
 

test_definite_hang.smt2

@@ -0,0 +1,2 @@
+(define-funs-rec ((loop ((x Int)) Int)) ((loop x)))
+(assert (= (loop 1) 0))

test_issue_with_checksat.smt2

@@ -0,0 +1,3 @@
+(define-funs-rec ((g ((a Int) (b Int)) Bool)) ((or (= a b) (ite (> a b) (g (- a 1) b) (g a (- b 1))))))
+(assert (g 2 2))
+(check-sat)

test_just_define.smt2

@@ -0,0 +1 @@
+(define-funs-rec ((g ((a Int) (b Int)) Bool)) ((or (= a b) (ite (> a b) (g (- a 1) b) (g a (- b 1))))))

test_simple_hang.smt2

@@ -0,0 +1,2 @@
+(define-funs-rec ((simple ((x Int)) Int)) ((ite (= x 0) 0 (simple (- x 1)))))
+(assert (= (simple 1) 0))