From 0a26bcf14c5db9697d0bba9d6e92f095a19e1285 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Nov 2015 15:12:08 -0500 Subject: [PATCH] ensure unique symbols when MaxSAT problems are extracted from linear objectives such that multiple objectives can be supported. Fixes issue #308 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 49b5f988f..1b4b1e7bc 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -770,7 +770,7 @@ namespace opt { tout << "offset: " << offset << "\n"; ); std::ostringstream out; - out << mk_pp(orig_term, m); + out << mk_pp(orig_term, m) << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -793,7 +793,7 @@ namespace opt { } neg = true; std::ostringstream out; - out << mk_pp(orig_term, m); + out << mk_pp(orig_term, m) << ":" << index; id = symbol(out.str().c_str()); return true; } @@ -812,7 +812,7 @@ namespace opt { } neg = is_max; std::ostringstream out; - out << mk_pp(orig_term, m); + out << mk_pp(orig_term, m) << ":" << index; id = symbol(out.str().c_str()); return true; }