summaryrefslogtreecommitdiffstats
path: root/src/misc/extra/extraBddImage.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc/extra/extraBddImage.c')
-rw-r--r--src/misc/extra/extraBddImage.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/misc/extra/extraBddImage.c b/src/misc/extra/extraBddImage.c
index d21cfe23..23c1c682 100644
--- a/src/misc/extra/extraBddImage.c
+++ b/src/misc/extra/extraBddImage.c
@@ -838,7 +838,7 @@ int Extra_FindBestVariable( DdManager * dd,
int iVarBest, v;
double CostBest, CostCur;
- CostBest = 100000000000000;
+ CostBest = 100000000000000.0;
iVarBest = -1;
for ( v = 0; v < nVars; v++ )
if ( pVars[v] )