Fix one off for pdkind model. Fixes #52.

src/engine/pdkind/pdkind_engine.cpp

@@ -539,7 +539,7 @@ const system::trace_helper* pdkind_engine::get_trace() {
 
     // Get the model and add it to the trace
     model = solver->get_model();
-    d_trace->set_model(model, current_depth + 1, current_depth + cex_step);
+    d_trace->set_model(model, current_depth, current_depth + cex_step);
 
     // Done, pop the solver scope
     scope.pop();

test/regress/issues/51.mcmt

@@ -0,0 +1,52 @@
+(define-state-type
+   S
+   (
+     (p Int)
+     (p_del Int)
+     (p_nil Bool)
+     (x Int)
+     (x_del Int)
+     (x_nil Bool)
+     (y Int)
+     (y_del Int)
+     (y_nil Bool))
+   ())
+(define-transition-system
+   TS
+   S
+   (and
+      (= y x)
+      (= y_del x_del)
+      (= y_nil true)
+      (=
+         p
+         (+ 1 y))
+      (= p_del 0)
+      (=
+         p_nil
+         (or false y_nil))
+      (= 0 y_del)
+      (= x 1)
+      (= x_del 0)
+      (= x_nil false))
+   (and
+      (= next.y state.x)
+      (= next.y_del state.x_del)
+      (= next.y_nil state.x_nil)
+      (=
+         next.p
+         (+ 1 next.y))
+      (= next.p_del 0)
+      (=
+         next.p_nil
+         (or false next.y_nil))
+      (= 0 next.y_del)
+      (= next.x next.p)
+      (= next.x_del next.p_del)
+      (= next.x_nil next.p_nil)))
+(query
+   TS
+   (= x 1))
+(query
+   TS
+   (= x 2))

test/regress/issues/51.mcmt.gold

@@ -0,0 +1 @@
+invalid.*

test/regress/issues/51.mcmt.options

@@ -0,0 +1 @@
+--engine pdkind --show-trace

test/regress/issues/52.mcmt

@@ -0,0 +1,12 @@
+(define-state-type
+   S
+   ((x Int))
+   ((i Int)))
+(define-transition-system
+   TS
+   S
+   (= x 0)
+   (= next.x (+ state.x 1)))
+(query
+   TS
+   (< x 10))

test/regress/issues/52.mcmt.gold

@@ -0,0 +1 @@
+invalid.*

test/regress/issues/52.mcmt.options

@@ -0,0 +1 @@
+--engine pdkind --show-trace