summaryrefslogtreecommitdiffstats
path: root/src/proof/int/int.h
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-04-28 16:55:25 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-04-28 16:55:25 -0700
commit9e1765216ba5f64d89a0dc93e33fb95c84a0c779 (patch)
treea3a35a93e30f5e22f22ee0a8fd51f5d12107d23a /src/proof/int/int.h
parent266667d8b231721c060495e7fb737e35bfbe575b (diff)
downloadabc-9e1765216ba5f64d89a0dc93e33fb95c84a0c779.tar.gz
abc-9e1765216ba5f64d89a0dc93e33fb95c84a0c779.tar.bz2
abc-9e1765216ba5f64d89a0dc93e33fb95c84a0c779.zip
Added option 'int -I <filename>' to specify file names to dump invariants.
Diffstat (limited to 'src/proof/int/int.h')
-rw-r--r--src/proof/int/int.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/int/int.h b/src/proof/int/int.h
index 97d628b4..906d8aaf 100644
--- a/src/proof/int/int.h
+++ b/src/proof/int/int.h
@@ -66,6 +66,7 @@ struct Inter_ManParams_t_
int fDropInvar; // dump inductive invariant into file
int fVerbose; // print verbose statistics
int iFrameMax; // the time frame reached
+ char * pFileName; // file name to dump interpolant
};
////////////////////////////////////////////////////////////////////////