From 493671aa7285a333379fed13f761b3cf50ff5243 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 26 Mar 2020 09:58:06 -0700
Subject: [PATCH] fix #3520

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/solver/solver_na2as.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index 6173dfddf..4f284a2d6 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -83,9 +83,10 @@ lbool solver_na2as::find_mutexes(expr_ref_vector const& vars, vector<expr_ref_ve
 }
 
 
-void solver_na2as::push() {
-    m_scopes.push_back(m_assumptions.size());
+void solver_na2as::push() {    
+    unsigned n = m_assumptions.size();
     push_core();
+    m_scopes.push_back(n);
 }
 
 void solver_na2as::pop(unsigned n) {