📔
HackTricks - Boitatech
  • HackTricks
  • About the author
  • Getting Started in Hacking
  • Pentesting Methodology
  • External Recon Methodology
    • Github Leaked Secrets
  • Phishing Methodology
    • Clone a Website
    • Detecting Phising
    • Phishing Documents
  • Exfiltration
  • Tunneling and Port Forwarding
  • Brute Force - CheatSheet
  • Search Exploits
  • Shells
    • Shells (Linux, Windows, MSFVenom)
      • MSFVenom - CheatSheet
      • Shells - Windows
      • Shells - Linux
      • Full TTYs
  • Linux/Unix
    • Checklist - Linux Privilege Escalation
    • Linux Privilege Escalation
      • PAM - Pluggable Authentication Modules
      • SELinux
      • Logstash
      • AppArmor
      • Containerd (ctr) Privilege Escalation
      • Docker Breakout
      • electron/CEF/chromium debugger abuse
      • Escaping from Jails
      • Cisco - vmanage
      • D-Bus Enumeration & Command Injection Privilege Escalation
      • Interesting Groups - Linux PE
        • lxd/lxc Group - Privilege escalation
      • ld.so exploit example
      • Linux Capabilities
      • NFS no_root_squash/no_all_squash misconfiguration PE
      • Payloads to execute
      • RunC Privilege Escalation
      • Seccomp
      • Splunk LPE and Persistence
      • SSH Forward Agent exploitation
      • Socket Command Injection
      • Wildcards Spare tricks
    • Useful Linux Commands
      • Bypass Bash Restrictions
    • Linux Environment Variables
  • MacOS
    • MacOS Security & Privilege Escalation
      • Mac OS Architecture
      • MacOS MDM
        • Enrolling Devices in Other Organisations
      • MacOS Protocols
      • MacOS Red Teaming
      • MacOS Serial Number
      • MacOS Apps - Inspecting, debugging and Fuzzing
  • Windows
    • Checklist - Local Windows Privilege Escalation
    • Windows Local Privilege Escalation
      • AppendData/AddSubdirectory permission over service registry
      • Create MSI with WIX
      • DPAPI - Extracting Passwords
      • SeImpersonate from High To System
      • Access Tokens
      • ACLs - DACLs/SACLs/ACEs
      • Dll Hijacking
      • From High Integrity to SYSTEM with Name Pipes
      • Integrity Levels
      • JAWS
      • JuicyPotato
      • Leaked Handle Exploitation
      • MSI Wrapper
      • Named Pipe Client Impersonation
      • PowerUp
      • Privilege Escalation Abusing Tokens
      • Privilege Escalation with Autoruns
      • RottenPotato
      • Seatbelt
      • SeDebug + SeImpersonate copy token
      • Windows C Payloads
    • Active Directory Methodology
      • Abusing Active Directory ACLs/ACEs
      • AD information in printers
      • ASREPRoast
      • BloodHound
      • Constrained Delegation
      • Custom SSP
      • DCShadow
      • DCSync
      • DSRM Credentials
      • Golden Ticket
      • Kerberos Authentication
      • Kerberoast
      • MSSQL Trusted Links
      • Over Pass the Hash/Pass the Key
      • Pass the Ticket
      • Password Spraying
      • Force NTLM Privileged Authentication
      • Privileged Accounts and Token Privileges
      • Resource-based Constrained Delegation
      • Security Descriptors
      • Silver Ticket
      • Skeleton Key
      • Unconstrained Delegation
    • NTLM
      • Places to steal NTLM creds
      • PsExec/Winexec/ScExec
      • SmbExec/ScExec
      • WmicExec
      • AtExec / SchtasksExec
      • WinRM
    • Stealing Credentials
      • Credentials Protections
      • Mimikatz
    • Authentication, Credentials, UAC and EFS
    • Basic CMD for Pentesters
    • Basic PowerShell for Pentesters
      • PowerView
    • AV Bypass
  • Mobile Apps Pentesting
    • Android APK Checklist
    • Android Applications Pentesting
      • Android Applications Basics
      • Android Task Hijacking
      • ADB Commands
      • APK decompilers
      • AVD - Android Virtual Device
      • Burp Suite Configuration for Android
      • content:// protocol
      • Drozer Tutorial
        • Exploiting Content Providers
      • Exploiting a debuggeable applciation
      • Frida Tutorial
        • Frida Tutorial 1
        • Frida Tutorial 2
        • Frida Tutorial 3
        • Objection Tutorial
      • Google CTF 2018 - Shall We Play a Game?
      • Inspeckage Tutorial
      • Intent Injection
      • Make APK Accept CA Certificate
      • Manual DeObfuscation
      • React Native Application
      • Reversing Native Libraries
      • Smali - Decompiling/[Modifying]/Compiling
      • Spoofing your location in Play Store
      • Webview Attacks
    • iOS Pentesting Checklist
    • iOS Pentesting
      • Basic iOS Testing Operations
      • Burp Suite Configuration for iOS
      • Extracting Entitlements From Compiled Application
      • Frida Configuration in iOS
      • iOS App Extensions
      • iOS Basics
      • iOS Custom URI Handlers / Deeplinks / Custom Schemes
      • iOS Hooking With Objection
      • iOS Protocol Handlers
      • iOS Serialisation and Encoding
      • iOS Testing Environment
      • iOS UIActivity Sharing
      • iOS Universal Links
      • iOS UIPasteboard
      • iOS WebViews
  • Pentesting
    • Pentesting Network
      • Spoofing LLMNR, NBT-NS, mDNS/DNS and WPAD and Relay Attacks
      • Spoofing SSDP and UPnP Devices with EvilSSDP
      • Wifi Attacks
        • Evil Twin EAP-TLS
      • Pentesting IPv6
      • Nmap Summary (ESP)
      • Network Protocols Explained (ESP)
      • IDS and IPS Evasion
      • DHCPv6
    • Pentesting JDWP - Java Debug Wire Protocol
    • Pentesting Printers
      • Accounting bypass
      • Buffer Overflows
      • Credentials Disclosure / Brute-Force
      • Cross-Site Printing
      • Document Processing
      • Factory Defaults
      • File system access
      • Firmware updates
      • Memory Access
      • Physical Damage
      • Software packages
      • Transmission channel
      • Print job manipulation
      • Print Job Retention
      • Scanner and Fax
    • Pentesting SAP
    • Pentesting Kubernetes
      • Enumeration from a Pod
      • Hardening Roles/ClusterRoles
      • Pentesting Kubernetes from the outside
    • 7/tcp/udp - Pentesting Echo
    • 21 - Pentesting FTP
      • FTP Bounce attack - Scan
      • FTP Bounce - Download 2ºFTP file
    • 22 - Pentesting SSH/SFTP
    • 23 - Pentesting Telnet
    • 25,465,587 - Pentesting SMTP/s
      • SMTP - Commands
    • 43 - Pentesting WHOIS
    • 53 - Pentesting DNS
    • 69/UDP TFTP/Bittorrent-tracker
    • 79 - Pentesting Finger
    • 80,443 - Pentesting Web Methodology
      • 403 & 401 Bypasses
      • AEM - Adobe Experience Cloud
      • Apache
      • Artifactory Hacking guide
      • Buckets
        • Firebase Database
        • AWS-S3
      • CGI
      • Code Review Tools
      • Drupal
      • Flask
      • Git
      • Golang
      • GraphQL
      • H2 - Java SQL database
      • IIS - Internet Information Services
      • JBOSS
      • Jenkins
      • JIRA
      • Joomla
      • JSP
      • Laravel
      • Moodle
      • Nginx
      • PHP Tricks (SPA)
        • PHP - Useful Functions & disable_functions/open_basedir bypass
          • disable_functions bypass - php-fpm/FastCGI
          • disable_functions bypass - dl function
          • disable_functions bypass - PHP 7.0-7.4 (*nix only)
          • disable_functions bypass - Imagick <= 3.3.0 PHP >= 5.4 Exploit
          • disable_functions - PHP 5.x Shellshock Exploit
          • disable_functions - PHP 5.2.4 ionCube extension Exploit
          • disable_functions bypass - PHP <= 5.2.9 on windows
          • disable_functions bypass - PHP 5.2.4 and 5.2.5 PHP cURL
          • disable_functions bypass - PHP safe_mode bypass via proc_open() and custom environment Exploit
          • disable_functions bypass - PHP Perl Extension Safe_mode Bypass Exploit
          • disable_functions bypass - PHP 5.2.3 - Win32std ext Protections Bypass
          • disable_functions bypass - PHP 5.2 - FOpen Exploit
          • disable_functions bypass - via mem
          • disable_functions bypass - mod_cgi
          • disable_functions bypass - PHP 4 >= 4.2.0, PHP 5 pcntl_exec
      • Python
      • Special HTTP headers
      • Spring Actuators
      • Symphony
      • Tomcat
      • Uncovering CloudFlare
      • VMWare (ESX, VCenter...)
      • Web API Pentesting
      • WebDav
      • werkzeug
      • Wordpress
      • XSS to RCE Electron Desktop Apps
    • 88tcp/udp - Pentesting Kerberos
      • Harvesting tickets from Windows
      • Harvesting tickets from Linux
    • 110,995 - Pentesting POP
    • 111/TCP/UDP - Pentesting Portmapper
    • 113 - Pentesting Ident
    • 123/udp - Pentesting NTP
    • 135, 593 - Pentesting MSRPC
    • 137,138,139 - Pentesting NetBios
    • 139,445 - Pentesting SMB
    • 143,993 - Pentesting IMAP
    • 161,162,10161,10162/udp - Pentesting SNMP
      • SNMP RCE
    • 194,6667,6660-7000 - Pentesting IRC
    • 264 - Pentesting Check Point FireWall-1
    • 389, 636, 3268, 3269 - Pentesting LDAP
    • 500/udp - Pentesting IPsec/IKE VPN
    • 502 - Pentesting Modbus
    • 512 - Pentesting Rexec
    • 513 - Pentesting Rlogin
    • 514 - Pentesting Rsh
    • 515 - Pentesting Line Printer Daemon (LPD)
    • 548 - Pentesting Apple Filing Protocol (AFP)
    • 554,8554 - Pentesting RTSP
    • 623/UDP/TCP - IPMI
    • 631 - Internet Printing Protocol(IPP)
    • 873 - Pentesting Rsync
    • 1026 - Pentesting Rusersd
    • 1080 - Pentesting Socks
    • 1098/1099/1050 - Pentesting Java RMI - RMI-IIOP
    • 1433 - Pentesting MSSQL - Microsoft SQL Server
    • 1521,1522-1529 - Pentesting Oracle TNS Listener
      • Oracle Pentesting requirements installation
      • TNS Poison
      • Remote stealth pass brute force
      • Oracle RCE & more
    • 1723 - Pentesting PPTP
    • 1883 - Pentesting MQTT (Mosquitto)
    • 2049 - Pentesting NFS Service
    • 2301,2381 - Pentesting Compaq/HP Insight Manager
    • 2375, 2376 Pentesting Docker
    • 3128 - Pentesting Squid
    • 3260 - Pentesting ISCSI
    • 3299 - Pentesting SAPRouter
    • 3306 - Pentesting Mysql
    • 3389 - Pentesting RDP
    • 3632 - Pentesting distcc
    • 3690 - Pentesting Subversion (svn server)
    • 4369 - Pentesting Erlang Port Mapper Daemon (epmd)
    • 5000 - Pentesting Docker Registry
    • 5353/UDP Multicast DNS (mDNS)
    • 5432,5433 - Pentesting Postgresql
    • 5601 - Pentesting Kibana
    • 5671,5672 - Pentesting AMQP
    • 5800,5801,5900,5901 - Pentesting VNC
    • 5984,6984 - Pentesting CouchDB
    • 5985,5986 - Pentesting WinRM
    • 6000 - Pentesting X11
    • 6379 - Pentesting Redis
    • 8009 - Pentesting Apache JServ Protocol (AJP)
    • 8089 - Splunkd
    • 9000 - Pentesting FastCGI
    • 9001 - Pentesting HSQLDB
    • 9042/9160 - Pentesting Cassandra
    • 9100 - Pentesting Raw Printing (JetDirect, AppSocket, PDL-datastream)
    • 9200 - Pentesting Elasticsearch
    • 10000 - Pentesting Network Data Management Protocol (ndmp)
    • 11211 - Pentesting Memcache
    • 15672 - Pentesting RabbitMQ Management
    • 27017,27018 - Pentesting MongoDB
    • 44818/UDP/TCP - Pentesting EthernetIP
    • 47808/udp - Pentesting BACNet
    • 50030,50060,50070,50075,50090 - Pentesting Hadoop
  • Pentesting Web
    • Web Vulnerabilities Methodology
    • Reflecting Techniques - PoCs and Polygloths CheatSheet
      • Web Vulns List
    • 2FA/OTP Bypass
    • Abusing hop-by-hop headers
    • Bypass Payment Process
    • Captcha Bypass
    • Cache Poisoning and Cache Deception
    • Clickjacking
    • Client Side Template Injection (CSTI)
    • Command Injection
    • Content Security Policy (CSP) Bypass
    • Cookies Hacking
    • CORS - Misconfigurations & Bypass
    • CRLF (%0D%0A) Injection
    • Cross-site WebSocket hijacking (CSWSH)
    • CSRF (Cross Site Request Forgery)
    • Dangling Markup - HTML scriptless injection
    • Deserialization
      • NodeJS - __proto__ & prototype Pollution
      • Java JSF ViewState (.faces) Deserialization
      • Java DNS Deserialization, GadgetProbe and Java Deserialization Scanner
      • Basic Java Deserialization (ObjectInputStream, readObject)
      • CommonsCollection1 Payload - Java Transformers to Rutime exec() and Thread Sleep
      • Basic .Net deserialization (ObjectDataProvider gadget, ExpandedWrapper, and Json.Net)
      • Exploiting __VIEWSTATE knowing the secrets
      • Exploiting __VIEWSTATE without knowing the secrets
    • Domain/Subdomain takeover
    • Email Header Injection
    • File Inclusion/Path traversal
      • phar:// deserialization
    • File Upload
      • PDF Upload - XXE and CORS bypass
    • Formula Injection
    • HTTP Request Smuggling / HTTP Desync Attack
    • H2C Smuggling
    • IDOR
    • JWT Vulnerabilities (Json Web Tokens)
    • NoSQL injection
    • LDAP Injection
    • Login Bypass
      • Login bypass List
    • OAuth to Account takeover
    • Open Redirect
    • Parameter Pollution
    • PostMessage Vulnerabilities
    • Race Condition
    • Rate Limit Bypass
    • Registration Vulnerabilities
    • Regular expression Denial of Service - ReDoS
    • Reset/Forgotten Password Bypass
    • SAML Attacks
      • SAML Basics
    • Server Side Inclusion/Edge Side Inclusion Injection
    • SQL Injection
      • MSSQL Injection
      • Oracle injection
      • PostgreSQL injection
        • dblink/lo_import data exfiltration
        • PL/pgSQL Password Bruteforce
        • Network - Privesc, Port Scanner and NTLM chanllenge response disclosure
        • Big Binary Files Upload (PostgreSQL)
        • RCE with PostgreSQL Extensions
      • MySQL injection
        • Mysql SSRF
      • SQLMap - Cheetsheat
        • Second Order Injection - SQLMap
    • SSRF (Server Side Request Forgery)
    • SSTI (Server Side Template Injection)
      • EL - Expression Language
    • Reverse Tab Nabbing
    • Unicode Normalization vulnerability
    • Web Tool - WFuzz
    • XPATH injection
    • XSLT Server Side Injection (Extensible Stylesheet Languaje Transformations)
    • XXE - XEE - XML External Entity
    • XSS (Cross Site Scripting)
      • PDF Injection
      • DOM XSS
      • Server Side XSS (Dynamic PDF)
      • XSS Tools
    • XSSI (Cross-Site Script Inclusion)
    • XS-Search
  • Forensics
    • Basic Forensic Methodology
      • Baseline Monitoring
      • Anti-Forensic Techniques
      • Docker Forensics
      • Image Adquisition & Mount
      • Linux Forensics
      • Malware Analysis
      • Memory dump analysis
        • Volatility - CheatSheet
      • Partitions/File Systems/Carving
        • EXT
        • File/Data Carving & Recovery Tools
        • NTFS
      • Pcap Inspection
        • DNSCat pcap analysis
        • USB Keystrokes
        • Wifi Pcap Analysis
        • Wireshark tricks
      • Specific Software/File-Type Tricks
        • .pyc
        • Browser Artifacts
        • Desofuscation vbs (cscript.exe)
        • Local Cloud Storage
        • Office file analysis
        • PDF File analysis
        • PNG tricks
        • Video and Audio file analysis
        • ZIPs tricks
      • Windows Artifacts
        • Windows Processes
        • Interesting Windows Registry Keys
  • A.I. Exploiting
    • BRA.I.NSMASHER Presentation
      • Basic Bruteforcer
      • Basic Captcha Breaker
      • BIM Bruteforcer
      • Hybrid Malware Classifier Part 1
  • Blockchain
    • Blockchain & Crypto Currencies
  • Courses and Certifications Reviews
    • INE Courses and eLearnSecurity Certifications Reviews
  • Cloud Security
    • Cloud security review
    • AWS Security
  • Physical attacks
    • Physical Attacks
    • Escaping from KIOSKs
      • Show file extensions
  • Reversing
    • Reversing Tools & Basic Methods
      • Angr
        • Angr - Examples
      • Z3 - Satisfiability Modulo Theories (SMT)
      • Cheat Engine
      • Blobrunner
    • Common API used in Malware
    • Cryptographic/Compression Algorithms
      • Unpacking binaries
    • Word Macros
  • Exploiting
    • Linux Exploiting (Basic) (SPA)
      • Format Strings Template
      • ROP - call sys_execve
      • ROP - Leaking LIBC address
        • ROP - Leaking LIBC template
      • Bypassing Canary & PIE
      • Ret2Lib
      • Fusion
    • Exploiting Tools
      • PwnTools
    • Windows Exploiting (Basic Guide - OSCP lvl)
  • Cryptography
    • Certificates
    • Cipher Block Chaining CBC-MAC
    • Crypto CTFs Tricks
    • Electronic Code Book (ECB)
    • Hash Length Extension Attack
    • Padding Oracle
    • RC4 - Encrypt&Decrypt
  • BACKDOORS
    • Merlin
    • Empire
    • Salseo
    • ICMPsh
  • Stego
    • Stego Tricks
    • Esoteric languages
  • MISC
    • Basic Python
      • venv
      • Bypass Python sandboxes
      • Magic Methods
      • Web Requests
      • Bruteforce hash (few chars)
    • Other Big References
  • TODO
    • More Tools
    • MISC
    • Pentesting DNS
  • Burp Suite
  • Other Web Tricks
  • Interesting HTTP
  • Emails Vulnerabilities
  • Android Forensics
  • TR-069
  • 6881/udp - Pentesting BitTorrent
  • CTF Write-ups
    • challenge-0521.intigriti.io
    • Try Hack Me
      • hc0n Christmas CTF - 2019
      • Pickle Rick
  • 1911 - Pentesting fox
  • Online Platforms with API
  • Stealing Sensitive Information Disclosure from a Web
  • Post Exploitation
Powered by GitBook
On this page
  • Basic Operations
  • Booleans/And/Or/Not
  • Ints/Simplify/Reals
  • Printing Model
  • Machine Arithmetic
  • Signed/Unsigned Numbers
  • Functions
  • Examples
  • Sudoku solver
  • References

Was this helpful?

  1. Reversing
  2. Reversing Tools & Basic Methods

Z3 - Satisfiability Modulo Theories (SMT)

Very basically, this tool will help us to find values for variables that need to satisfy some conditions and calculating them by hand will be so annoying. Therefore, you can indicate to Z3 the conditions the variables need to satisfy and it will find some values (if possible).

Basic Operations

Booleans/And/Or/Not

#pip3 install z3-solver
from z3 import *
s = Solver() #The solver will be given the conditions

x = Bool("x") #Declare the symbos x, y and z
y = Bool("y")
z = Bool("z")

# (x or y or !z) and y
s.add(And(Or(x,y,Not(z)),y))
s.check() #If response is "sat" then the model is satifable, if "unsat" something is wrong
print(s.model()) #Print valid values to satisfy the model

Ints/Simplify/Reals

from z3 import *

x = Int('x')
y = Int('y')
#Simplify a "complex" ecuation
print(simplify(And(x + 1 >= 3, x**2 + x**2 + y**2 + 2 >= 5)))
#And(x >= 2, 2*x**2 + y**2 >= 3)

#Note that Z3 is capable to treat irrational numbers (An irrational algebraic number is a root of a polynomial with integer coefficients. Internally, Z3 represents all these numbers precisely.)
#so you can get the decimals you need from the solution
r1 = Real('r1')
r2 = Real('r2')
#Solve the ecuation
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))
#Solve the ecuation with 30 decimals
set_option(precision=30)
print(solve(r1**2 + r2**2 == 3, r1**3 == 2))

Printing Model

from z3 import *

x, y, z = Reals('x y z')
s = Solver()
s.add(x > 1, y > 1, x + y > 3, z - x < 10)
s.check()

m = s.model()
print ("x = %s" % m[x])
for d in m.decls():
    print("%s = %s" % (d.name(), m[d]))

Machine Arithmetic

Modern CPUs and main-stream programming languages use arithmetic over fixed-size bit-vectors. Machine arithmetic is available in Z3Py as Bit-Vectors.

from z3 import *

x = BitVec('x', 16) #Bit vector variable "x" of length 16 bit
y = BitVec('y', 16)

e = BitVecVal(10, 16) #Bit vector with value 10 of length 16bits
a = BitVecVal(-1, 16)
b = BitVecVal(65535, 16)
print(simplify(a == b)) #This is True!
a = BitVecVal(-1, 32)
b = BitVecVal(65535, 32)
print(simplify(a == b)) #This is False

Signed/Unsigned Numbers

Z3 provides special signed versions of arithmetical operations where it makes a difference whether the bit-vector is treated as signed or unsigned. In Z3Py, the operators <, <=, >, >=, /, % and >> correspond to the signed versions. The corresponding unsigned operators are ULT, ULE, UGT, UGE, UDiv, URem and LShR.

from z3 import *

# Create to bit-vectors of size 32
x, y = BitVecs('x y', 32)
solve(x + y == 2, x > 0, y > 0)

# Bit-wise operators
# & bit-wise and
# | bit-wise or
# ~ bit-wise not
solve(x & y == ~y)
solve(x < 0)

# using unsigned version of < 
solve(ULT(x, 0))

Functions

Interpreted functions such as arithmetic where the function + has a fixed standard interpretation (it adds two numbers). Uninterpreted functions and constants are maximally flexible; they allow any interpretation that is consistent with the constraints over the function or constant.

Example: f applied twice to x results in x again, but f applied once to x is different from x.

from z3 import *

x = Int('x')
y = Int('y')
f = Function('f', IntSort(), IntSort())
s = Solver()
s.add(f(f(x)) == x, f(x) == y, x != y)
s.check()
m = s.model()
print("f(f(x)) =", m.evaluate(f(f(x))))
print("f(x)    =", m.evaluate(f(x)))

print(m.evaluate(f(2)))
s.add(f(x) == 4) #Find the value that generates 4 as response
s.check()
print(m.model())

Examples

Sudoku solver

# 9x9 matrix of integer variables
X = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(9) ]
      for i in range(9) ]

# each cell contains a value in {1, ..., 9}
cells_c  = [ And(1 <= X[i][j], X[i][j] <= 9)
             for i in range(9) for j in range(9) ]

# each row contains a digit at most once
rows_c   = [ Distinct(X[i]) for i in range(9) ]

# each column contains a digit at most once
cols_c   = [ Distinct([ X[i][j] for i in range(9) ])
             for j in range(9) ]

# each 3x3 square contains a digit at most once
sq_c     = [ Distinct([ X[3*i0 + i][3*j0 + j]
                        for i in range(3) for j in range(3) ])
             for i0 in range(3) for j0 in range(3) ]

sudoku_c = cells_c + rows_c + cols_c + sq_c

# sudoku instance, we use '0' for empty cells
instance = ((0,0,0,0,9,4,0,3,0),
            (0,0,0,5,1,0,0,0,7),
            (0,8,9,0,0,0,0,4,0),
            (0,0,0,0,0,0,2,0,8),
            (0,6,0,2,0,1,0,5,0),
            (1,0,2,0,0,0,0,0,0),
            (0,7,0,0,0,0,5,2,0),
            (9,0,0,0,6,5,0,0,0),
            (0,4,0,9,7,0,0,0,0))

instance_c = [ If(instance[i][j] == 0,
                  True,
                  X[i][j] == instance[i][j])
               for i in range(9) for j in range(9) ]

s = Solver()
s.add(sudoku_c + instance_c)
if s.check() == sat:
    m = s.model()
    r = [ [ m.evaluate(X[i][j]) for j in range(9) ]
          for i in range(9) ]
    print_matrix(r)
else:
    print "failed to solve"

References

PreviousAngr - ExamplesNextCheat Engine

Last updated 3 years ago

Was this helpful?

https://ericpony.github.io/z3py-tutorial/guide-examples.htm