Fix typo: Satifiability to Satisfiability

symbolic_execution/language/bitcoin/symbolic_interpreter.py

@@ -24,7 +24,7 @@ from z3 import *
 import numpy as np
 from symbolic_execution.program.block.utils import compute_path_count
 
-class Satifiability(Enum):
+class Satisfiability(Enum):
     SATISFIABLE = 0
     UNSATISFIABLE = 1
     UNKNOWN = 2
@@ -76,21 +76,21 @@ def __find_unlocking_script_timed(hex_script, return_dict, verbose, count_path):
         if satisfiability == sat:
             m = s.model()
 
-        return_dict["satisfiability"] = Satifiability.z3_to_enum(satisfiability)
+        return_dict["satisfiability"] = Satisfiability.z3_to_enum(satisfiability)
         return_dict["model"] = str(m)
         if count_path:
             return_dict["path_count"] = compute_path_count(program)
 
     except InvalidOpCode as e:
-        return_dict["satisfiability"] = Satifiability.UNSPENDABLE
+        return_dict["satisfiability"] = Satisfiability.UNSPENDABLE
         return_dict["model"] = {}
 
     except IncompleteIfEndIfClause as e:
-        return_dict["satisfiability"] = Satifiability.UNSPENDABLE
+        return_dict["satisfiability"] = Satisfiability.UNSPENDABLE
         return_dict["model"] = {}
 
     except UnimplementedInstructionError as e:
-        return_dict["satisfiability"] = Satifiability.UNSPENDABLE
+        return_dict["satisfiability"] = Satisfiability.UNSPENDABLE
         return_dict["model"] = {}
 
     except Exception as e:
@@ -114,7 +114,7 @@ def find_unlocking_script(hex_script: str, timeout=None, verbose=False, count_pa
     p1.terminate()
 
     if p1.exitcode is None:
-        return "", Satifiability.z3_to_enum(unknown), np.nan
+        return "", Satisfiability.z3_to_enum(unknown), np.nan
     elif count_path:
         return return_dict["model"], return_dict["satisfiability"], return_dict["path_count"]
     else: