mirror of
				https://github.com/Z3Prover/z3
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Merge branch 'master' into unit_prop_on_monomials
This commit is contained in:
		
						commit
						94eb101873
					
				
					 1 changed files with 1 additions and 1 deletions
				
			
		| 
						 | 
				
			
			@ -1805,7 +1805,7 @@ public:
 | 
			
		|||
        m_nla->check_bounded_divisions();
 | 
			
		||||
        for (auto & lemma : m_nla->lemmas())
 | 
			
		||||
            false_case_of_check_nla(lemma);
 | 
			
		||||
        return m_nla->lemmas().empty();        
 | 
			
		||||
        return m_nla->lemmas().empty();
 | 
			
		||||
    }
 | 
			
		||||
 | 
			
		||||
    expr_ref var2expr(lpvar v) {
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue