Adjust bound and witness when monitor state is added to TS (#356)

pono.cpp

@@ -97,11 +97,13 @@ ProverResult check_prop(PonoOptions pono_options,
     assert(!ts.inputvars().size());
   }
 
+  bool has_monitor = false;
   if (!ts.only_curr(prop)) {
     logger.log(1,
                "Got next state or input variables in property. "
                "Generating a monitor state.");
     prop = add_prop_monitor(ts, prop);
+    has_monitor = true;
   }
 
   if (pono_options.assume_prop_) {
@@ -141,11 +143,16 @@ ProverResult check_prop(PonoOptions pono_options,
   }
   else
   {
-    r = prover->check_until(pono_options.bound_);
+    r = prover->check_until(pono_options.bound_ + has_monitor);
   }
 
   if (r == FALSE && pono_options.witness_) {
     bool success = prover->witness(cex);
+    if (has_monitor) {
+      // Witness will always have at least one element, because the monitor is constrained
+      // to start true.
+      cex.pop_back();
+    }
     if (!success) {
       logger.log(
           0,