mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 00:35:47 +00:00
Code Activity

working on imdds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorne@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-08 11:53:54 -07:00
parent 1cfe6e477a
commit 78f29416f1
3 changed files with 572 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
lib/dl_bmc_engine.cpp
View file

@ -93,12 +93,12 @@ namespace datalog {
return l_false;
}
if (false && is_linear()) {
if (is_linear()) {
return check_linear();
}
else {
IF_VERBOSE(1, verbose_stream() << "non-linear BMC is not supported\n";);
// return l_undef;
return l_undef;
return check_nonlinear();
}
}