mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-07 09:55:20 +00:00
Code Activity

Minor bugfix in write_smt2

Browse source
This commit is contained in:
Clifford Wolf 2016-09-04 16:32:47 +02:00
parent 19a3b3732c
commit 372d672c2a
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
backends/smt2/smt2.cc
View file

@ -752,7 +752,7 @@ struct Smt2Worker
string assert_expr = assert_list.empty() ? "true" : "(and"; string assert_expr = assert_list.empty() ? "true" : "(and";
if (!assert_list.empty()) { if (!assert_list.empty()) {
if (GetSize(assert_list) == 1) { if (GetSize(assert_list) == 1) {
assert_expr = assert_list.front(); assert_expr = "\n " + assert_list.front() + "\n";
} else { } else {
for (auto &str : assert_list) for (auto &str : assert_list)
assert_expr += stringf("\n %s", str.c_str()); assert_expr += stringf("\n %s", str.c_str());
@ -765,7 +765,7 @@ struct Smt2Worker
string assume_expr = assume_list.empty() ? "true" : "(and"; string assume_expr = assume_list.empty() ? "true" : "(and";
if (!assume_list.empty()) { if (!assume_list.empty()) {
if (GetSize(assume_list) == 1) { if (GetSize(assume_list) == 1) {
assume_expr = assume_list.front(); assume_expr = "\n " + assume_list.front() + "\n";
} else { } else {
for (auto &str : assume_list) for (auto &str : assume_list)
assume_expr += stringf("\n %s", str.c_str()); assume_expr += stringf("\n %s", str.c_str());
@ -778,7 +778,7 @@ struct Smt2Worker
string init_expr = init_list.empty() ? "true" : "(and"; string init_expr = init_list.empty() ? "true" : "(and";
if (!init_list.empty()) { if (!init_list.empty()) {
if (GetSize(init_list) == 1) { if (GetSize(init_list) == 1) {
init_expr = init_list.front(); init_expr = "\n " + init_list.front() + "\n";
} else { } else {
for (auto &str : init_list) for (auto &str : init_list)
init_expr += stringf("\n %s", str.c_str()); init_expr += stringf("\n %s", str.c_str());