From f28edea6acdb48913c8d7ffc55fcdc047054c1ab Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sat, 8 Apr 2017 18:15:16 +0200
Subject: [PATCH] added constraint for ctx aut states in state equivallence
 encoding

---
 smt/smt_checker_rsc.py | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py
index 0aafe79..4604f87 100644
--- a/smt/smt_checker_rsc.py
+++ b/smt/smt_checker_rsc.py
@@ -472,6 +472,9 @@ class SmtCheckerRSC(object):
             e_i_equality = self.v[level_A][e_i] == self.v[level_B][e_i]
             eq_enc = simplify(And(eq_enc, e_i_equality))
 
+        eq_enc_ctxaut = self.ca_state[level_A] == self.ca_state[level_B]
+        eq_enc = simplify(And(eq_enc, eq_enc_ctxaut))
+
         return eq_enc
     
     def get_loop_encodings(self):