var fDesc=new Array();
fDesc[0] = "Z3 is an SMT solver that combines several theory solvers into a combined framework. It can be used to prove theorems and find counter-examples for non-theorems. Philippe Suter made a JNI binding available. There is also an existing Python binding by Sascha Boehme.<br /> Features:<br /> - Enable check_assumptions without enclosing push/pop. This resolves the limitation described in Limitations:<br /> - Expose coefficients used in arithmetical proofs.<br /> - Allow quantified theory axioms.<br /> - Fixes to the SMT-LIB 2.0 pretty printing mode.<br /> - Detect miss-annotated SMT-LIB benchmarks to avoid crashes when using the wrong solvers. Thanks to Trevor Hansen.<br /> - A digression in the managed API from 2.10 when passing null parameters.<br /> - Crash/incorrect handling of inequalities over the reals during quantifier elimination. Thanks to Mikkel Larsen Pedersen.<br /> - Bug in destructive equality resolution. Thanks to Sascha Boehme.<br /> - Bug in initialization for x64_mt executable on SMT benchmarks. Thanks to Alvin Cheung.";

function tShowHide(id, show)
{
	var s = document.getElementById("desc");

	if ((s.innerHTML.length<=212 || show==1) && show!=2)
	{
		s.innerHTML = fDesc[id];
		if (document.getElementById('m1'))
			document.getElementById('m1').style.display='none';
		if (document.getElementById('m2'))
			document.getElementById('m2').style.display='none';
		if (document.getElementById('more_txt'))
			document.getElementById('more_txt').style.display='inline';
	}
	else
	{
		s.innerHTML = '';
	}
}