Fix indexed free variables for states and percepts in Z3

learner_base.py

@@ -32,8 +32,9 @@ class Z3LearnerBase(LearnerBase):
     def __init__(self, state_dim, perc_dim) -> None:
         super().__init__()
         self._solver = z3.SolverFor('QF_LRA')
-        self._state_vars = z3.RealVarVector(state_dim)
-        self._percept_vars = z3.RealVarVector(perc_dim)
+        real_var_vec = z3.RealVarVector(state_dim + perc_dim)
+        self._state_vars = real_var_vec[0:state_dim]
+        self._percept_vars = real_var_vec[state_dim:state_dim+perc_dim]
 
     @property
     def state_dim(self) -> int:
@@ -47,5 +48,9 @@ class Z3LearnerBase(LearnerBase):
         res = self._solver.check()
         if res == z3.sat:
             return self._solver.model()
+        elif res == z3.unsat:
+            print("(unsat)")
+            return None
         else:
+            print("(unknown)")
             return None