diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java
index 759bc332e7..1c2ee0083b 100644
--- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java
+++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ItpSolver.java
@@ -244,7 +244,7 @@ public void push() {
 
     @Override
     public void pop(final int n) {
-        expCnt += n;
+        expCnt -= n;
         markers.pop(n);
         for (final Z3ItpMarker marker : markers) {
             marker.pop(n);