bugfix in yices solver

ucsb-seclab · May 28, 2024 · 502c61a · 502c61a
1 parent e0fe3f6
commit 502c61a
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/greed/solver/yices2.py b/greed/solver/yices2.py
@@ -572,7 +572,8 @@ def __init__(self, *args: YicesTermBool):
         self.args = list(args)
 
     def dump_smt2(self):
-        return f"(and {self.lhs.dump_smt2()} {self.rhs.dump_smt2()})"
+        and_args = ' '.join([arg.dump_smt2() for arg in self.args])
+        return f"(and {and_args})"
 
     def __getstate__(self):
         return {"args": self.args}
@@ -590,7 +591,8 @@ def __init__(self, *args: YicesTermBool):
         self.args = list(args)
 
     def dump_smt2(self):
-        return f"(or {self.lhs.dump_smt2()} {self.rhs.dump_smt2()})"
+        or_args = ' '.join([arg.dump_smt2() for arg in self.args])
+        return f"(or {or_args})"
 
     def __getstate__(self):
         return {"args": self.args}