Skip to content

Commit 5df5178

Browse files
tautschnigtautschnig
authored
Merge pull request #899 from diffblue/ic3-result
IC3: use report_results
2 parents 8975cd6 + 9063ef9 commit 5df5178

11 files changed

+70
-38
lines changed

‎regression/ebmc/ic3/bobcount.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
bobcount.sv
33
--ic3
4-
^EXIT=2$
5-
^SIGNAL=0$
4+
^\[bobcount\.assert\.1\] always !bobcount\.p0: PROVED$
65
^property HOLDS
76
^inductive invariant verification is ok
7+
^EXIT=2$
8+
^SIGNAL=0$
89
--
910
^inductive invariant verification failed

‎regression/ebmc/ic3/bobmiterbm1multi.1033.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.assert.1033
4-
^EXIT=2$
5-
^SIGNAL=0$
4+
^\[bobmiterbm1multi\.assert\.1033\] always !bobmiterbm1multi\.p1032: PROVED$
65
^property HOLDS
76
^inductive invariant verification is ok
7+
^EXIT=2$
8+
^SIGNAL=0$
89
--
910
^inductive invariant verification failed

‎regression/ebmc/ic3/bobmiterbm1multi.1080.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
bobmiterbm1multi.sv
33
--ic3 --property bobmiterbm1multi.assert.1080
4-
^EXIT=1$
5-
^SIGNAL=0$
4+
^\[bobmiterbm1multi\.assert\.1080\] always !bobmiterbm1multi\.p1079: REFUTED$
65
^property FAILED
76
^cex verification is ok
7+
^EXIT=1$
8+
^SIGNAL=0$
89
--
910
^cex verification failed

‎regression/ebmc/ic3/eijks208o.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
eijks208o.sv
33
--ic3
4-
^EXIT=2$
5-
^SIGNAL=0$
4+
^\[eijks208o\.assert\.1\] always !eijks208o\.p0: PROVED$
65
^property HOLDS
76
^inductive invariant verification is ok
7+
^EXIT=2$
8+
^SIGNAL=0$
89
--
910
^inductive invariant verification failed

‎regression/ebmc/ic3/non_inductive1.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
non_inductive1.sv
33
--ic3 --property main.p0
4-
^EXIT=2$
5-
^SIGNAL=0$
4+
^\[main\.p0\] always main\.s11: PROVED$
65
^property HOLDS$
76
^inductive invariant verification is ok
7+
^EXIT=2$
8+
^SIGNAL=0$
89
--
910
^inductive invariant verification failed

‎regression/ebmc/ic3/pdtvispeterson.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
pdtvispeterson.sv
33
--ic3
4-
^EXIT=2$
5-
^SIGNAL=0$
4+
^\[pdtvispeterson\.assert\.1\] always !pdtvispeterson\.p0: PROVED$
65
^property HOLDS
76
^inductive invariant verification is ok
7+
^EXIT=2$
8+
^SIGNAL=0$
89
--
910
^inductive invariant verification failed

‎regression/ebmc/ic3/ringp0.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
ringp0.sv
33
--ic3
4-
^EXIT=1$
5-
^SIGNAL=0$
4+
^\[ringp0\.assert\.1\] always !ringp0\.p0: REFUTED$
65
^property FAILED
76
^cex verification is ok
7+
^EXIT=1$
8+
^SIGNAL=0$
89
--
910
^cex verification failed

‎regression/ebmc/ic3/sm98a7multi.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
sm98a7multi.sv
33
--ic3 --property sm98a7multi.assert.2 --constr
4-
^EXIT=1$
5-
^SIGNAL=0$
4+
^\[sm98a7multi\.assert\.2\] always !sm98a7multi\.p1: REFUTED$
65
^property FAILED
76
^cex verification is ok
7+
^EXIT=1$
8+
^SIGNAL=0$
89
--
910
^cex verification failed

‎regression/ebmc/ic3/visbakery.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
visbakery.sv
33
--ic3
4-
^EXIT=1$
5-
^SIGNAL=0$
4+
^\[visbakery\.assert\.1\] always !visbakery\.p0: REFUTED$
65
^property FAILED
76
^cex verification is ok
7+
^EXIT=1$
8+
^SIGNAL=0$
89
--
910
^cex verification failed

‎regression/ebmc/ic3/viseisenberg.desc

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,10 @@
11
CORE
22
viseisenberg.sv
33
--ic3
4-
^EXIT=1$
5-
^SIGNAL=0$
4+
^\[viseisenberg\.assert\.1\] always !viseisenberg\.p0: REFUTED$
65
^property FAILED
76
^cex verification is ok
7+
^EXIT=1$
8+
^SIGNAL=0$
89
--
910
^cex verification failed

‎src/ic3/m1ain.cc

Lines changed: 40 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -141,6 +141,46 @@ int ic3_enginet::operator()()
141141
report_results(cmdline, result, ns, message.get_message_handler());
142142
return result.exit_code();
143143
}
144+
145+
const0 = false;
146+
const1 = false;
147+
orig_names = false;
148+
149+
// print_nodes();
150+
// print_var_map(std::cout);
151+
read_ebmc_input();
152+
// print_blif3("tst.blif",Ci.N);
153+
if (cmdline.isset("aiger")) {
154+
printf("converting to aiger format\n");
155+
Ci.print_aiger_format();
156+
exit(0);
157+
}
158+
159+
// printf("Constr_gates.size() = %d\n",Ci.Constr_gates.size());
160+
int result = Ci.run_ic3();
161+
162+
// find the first unknown property
163+
for(auto &property : properties.properties)
164+
{
165+
if(property.is_unknown())
166+
{
167+
switch(result)
168+
{
169+
case 1: property.refuted(); break;
170+
case 2: property.proved(); break;
171+
default: property.failure(); break;
172+
}
173+
break;
174+
}
175+
}
176+
177+
{
178+
property_checker_resultt result{properties};
179+
namespacet ns(transition_system.symbol_table);
180+
report_results(cmdline, result, ns, message.get_message_handler());
181+
}
182+
183+
return result;
144184
}
145185
catch(const std::string &error_str)
146186
{
@@ -154,24 +194,6 @@ int ic3_enginet::operator()()
154194
catch(int) {
155195
return 1;
156196
}
157-
158-
const0 = false;
159-
const1 = false;
160-
orig_names = false;
161-
162-
// print_nodes();
163-
// print_var_map(std::cout);
164-
read_ebmc_input();
165-
// print_blif3("tst.blif",Ci.N);
166-
if (cmdline.isset("aiger")) {
167-
printf("converting to aiger format\n");
168-
Ci.print_aiger_format();
169-
exit(0);
170-
}
171-
172-
// printf("Constr_gates.size() = %d\n",Ci.Constr_gates.size());
173-
return(Ci.run_ic3());
174-
175197
} /* end of function operator */
176198

177199
/* ======================

0 commit comments

Comments
 (0)