about summary refs log tree commit diff stats
path: root/test
diff options
context:
space:
mode:
Diffstat (limited to 'test')
-rw-r--r--test/ir/translators/smt2.py4
-rw-r--r--test/ir/translators/z3_ir.py17
2 files changed, 10 insertions, 11 deletions
diff --git a/test/ir/translators/smt2.py b/test/ir/translators/smt2.py
index 81f63b45..bf418f44 100644
--- a/test/ir/translators/smt2.py
+++ b/test/ir/translators/smt2.py
@@ -43,8 +43,8 @@ e_z3 = t_z3.from_expr(e)
 smt2 = t_smt2.to_smt2([t_smt2.from_expr(e)])
 
 # parse smt2 string with z3
-smt2_z3 = parse_smt2_string(smt2)
-
+result = parse_smt2_string(smt2)
+smt2_z3 = result[0]
 # initialise SMT solver
 s = Solver()
 
diff --git a/test/ir/translators/z3_ir.py b/test/ir/translators/z3_ir.py
index b28269fb..b96e43bb 100644
--- a/test/ir/translators/z3_ir.py
+++ b/test/ir/translators/z3_ir.py
@@ -24,13 +24,12 @@ def check_interp(interp, constraints, bits=32, valbits=8):
     constraints = dict((addr,
                         z3.BitVecVal(val, valbits))
                        for addr, val in constraints)
-    l = interp.as_list()
-    for entry in l:
-        if not isinstance(entry, list) or len(entry) < 2:
-            continue
-        addr, value = entry[0], entry[1]
-        if addr.as_long() in constraints:
-            assert equiv(value, constraints[addr.as_long()])
+    entry = interp.children()
+    assert len(entry) == 3
+    _, addr, value = entry
+    addr = addr.as_long()
+    assert addr in constraints
+    assert equiv(value, constraints[addr])
 
 # equiv short test
 # --------------------------------------------------------------------------
@@ -100,7 +99,7 @@ solver.add(ez3 == 10)
 solver.check()
 model = solver.model()
 check_interp(model[mem.get_mem_array(32)],
-             [(0xdeadbeef, 2), (0xdeadbeef + 3, 0)])
+             [(0xdeadbeef, 2)])
 
 # --------------------------------------------------------------------------
 ez3 = translator2.from_expr(e4)
@@ -116,7 +115,7 @@ solver.add(ez3 == 10)
 solver.check()
 model = solver.model()
 check_interp(model[memb.get_mem_array(32)],
-             [(0xdeadbeef, 0), (0xdeadbeef + 3, 2)])
+             [(0xdeadbeef+3, 2)])
 
 # --------------------------------------------------------------------------
 e5 = ExprSlice(ExprCompose(e, four), 0, 32) * five