From 93e08d9499c20dd23af35c4225b512b83abd86f2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 19 Sep 2017 19:43:23 -0700 Subject: [PATCH] fix #1261 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index e78c6388e..d624a5c9a 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -109,8 +109,10 @@ namespace smt { } virtual void assert_expr(expr * t, expr * a) { + if (m_name2assertion.contains(a)) { + throw default_exception("named assertion defined twice"); + } solver_na2as::assert_expr(t, a); - SASSERT(!m_name2assertion.contains(a)); get_manager().inc_ref(t); m_name2assertion.insert(a, t); }