Test case 3

backend/solver.py

@@ -126,6 +126,8 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content)
             stderr=subprocess.PIPE,
             text=True
         )
+        if result.stderr.strip():
+            return "error: " + result.stderr.strip()
         output = result.stdout.strip()
         return output.lower()
 
@@ -144,7 +146,12 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content)
         if "s.add" in line and "pos" in line:
             constraint = line.strip()
             cnt_cons += 1
-            if satisfied(constraint) == "unsat":
+            output = satisfied(constraint)
+            if "error" in output:
+                problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Error: {output}.\n"
+                ok_satisfied = False
+                break
+            if output == "unsat":
                 ok_satisfied = False
                 problematic_constraints += f"In line {i + 1}, the {cnt_cons}-th constraint: {constraint}. Not satisfied.\n"
     if ok_satisfied:
@@ -172,7 +179,7 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content)
     # print("\n".join(code_by_line_experiment) + sat_cnt_content)
     # print(res)
     if not res or res == "error":
-        problematic_constraints += f"Unable to judge: {res}, {"\n".join(code_by_line_experiment) + sat_cnt_content}"
+        problematic_constraints += f"Unable to judge."
     else:
         cur = int(res.split(':')[1])
         problematic_constraints += f"The number of solutions: {cur}\n"
@@ -182,7 +189,7 @@ def solve_puzzle(index, puzzle, expected_solution, sys_content, sat_cnt_content)
                 code_by_line_experiment[i] = ""
                 res = run_result()
                 if not res or res == "error":
-                    problematic_constraints += f"Unable to judge further: {res}, {"\n".join(code_by_line_experiment) + sat_cnt_content}"
+                    problematic_constraints += f"Unable to judge further."
                     break
                 now_cnt = int(res.split(':')[1])
                 if now_cnt == cur: