when number of operands are wrong, it throws error

[fzyzcjy]

e.g.

File /data/jychen/research/code/research_mono/neural_theorem_prover/evaluate.py:182, in _interact_with_prover_sequentially_single(initial_step, max_steps, debug_name, verbose)
    180 for action in actions:
    181     lemma, input_entities = prover.find_action(action)
--> 182     result = prover.inner.apply_theorem(lemma, input_entities)
    183     result_info = prover.interpret_result(result)
    185     if verbose:

File /data/jychen/research/code/third_party/INT/int_environment/proof_system/prover.py:169, in Prover.apply_theorem(self, theorem, operands)
    167 def apply_theorem(self, theorem, operands):
    168     # Apply a theorem with operands
--> 169     results = theorem.execute_th(operands, mode=self.mode_theorem)
    170     assumptions, conclusions = results["Assumptions"], results["Conclusions"]
    172     # Prevent the scenario [0, 1] -> [0]

File /data/jychen/research/code/third_party/INT/int_environment/proof_system/field_axioms.py:1364, in EquMoveTerm.execute_th(self, operands, mode)
   1359 elif mode == "prove":
   1360     """
   1361     a + b = c, ls(a) => ls(c + (-b))
   1362     2 inputs: [a, c + (-b)]
   1363     """
-> 1364     a, c_minus_b, = [deepcopy(op) for op in operands]
   1365     if is_entity(a) and is_entity(c_minus_b) and is_structured(c_minus_b, "add") \
   1366             and is_structured(c_minus_b.operands[1], "opp"):
   1367         c, minus_b, = c_minus_b.operands

ValueError: not enough values to unpack (expected 2, got 1)

[fzyzcjy]

anyway, except Exception to catch all currently as a hack

a better design is to verify the number of arguments before executing it