diff --git a/smt.py b/smt.py
index 0be7af6..3946975 100644
--- a/smt.py
+++ b/smt.py
@@ -230,7 +230,7 @@ class SMTLogicEncoder:
             for smt_elem in self.smt_carrier_set
         }
 
-        # Exclude operation function mappings
+        # Iterate over all logical operations
         for model_func in model.logical_operations:
             operation = Operation(model_func.operation_name, model_func.arity)
             smt_func = self.operation_function_map[operation]
@@ -239,10 +239,9 @@ class SMTLogicEncoder:
                 smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs)
                 smt_output = model_value_to_smt[output]
 
-                # For future models the input->output mapping may differ
+                # It may be the case that the output of f(input) differs
                 constraints.append(smt_func(*smt_inputs) != smt_output)
 
-        # Exclude designated value set
         for smt_elem in self.smt_carrier_set:
             model_val = ModelValue(str(smt_elem))
             is_designated_in_model = model_val in model.designated_values
diff --git a/vsp.py b/vsp.py
index 5ea2ae9..0de5b10 100644
--- a/vsp.py
+++ b/vsp.py
@@ -168,7 +168,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
                 )
             )
 
-    # x -> y is non-designated
+    # x -> y is non-designated for any x in K1 and y in K2
     smt_imp = encoder.model_function_map[impfn]
     for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
         encoder.solver.add(